diff src/elab_err.sig @ 623:588b9d16b00a

Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 16:10:25 -0500
parents 6a0e54400805
children 1fb318c17546
line wrap: on
line diff
--- a/src/elab_err.sig	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/elab_err.sig	Sun Feb 22 16:10:25 2009 -0500
@@ -27,11 +27,16 @@
 
 signature ELAB_ERR = sig
 
+    datatype kind_error =
+             UnboundKind of ErrorMsg.span * string
+
+    val kindError : ElabEnv.env -> kind_error -> unit
+
     datatype kunify_error =
              KOccursCheckFailed of Elab.kind * Elab.kind
            | KIncompatible of Elab.kind * Elab.kind
 
-    val kunifyError : kunify_error -> unit
+    val kunifyError : ElabEnv.env -> kunify_error -> unit
 
     datatype con_error =
              UnboundCon of ErrorMsg.span * string