diff src/elab_util.sig @ 1639:6c00d8af6239

Add a new scoping check for unification variables, to fix a type inference bug
author Adam Chlipala <adam@chlipala.net>
date Sun, 18 Dec 2011 11:29:13 -0500
parents c37d8341940a
children 4a03aa3251cb
line wrap: on
line diff
--- a/src/elab_util.sig	Sat Dec 17 20:42:39 2011 -0500
+++ b/src/elab_util.sig	Sun Dec 18 11:29:13 2011 -0500
@@ -64,6 +64,13 @@
     val map : {kind : Elab.kind' -> Elab.kind',
                con : Elab.con' -> Elab.con'}
               -> Elab.con -> Elab.con
+    val appB : {kind : 'context -> Elab.kind' -> unit,
+                con : 'context -> Elab.con' -> unit,
+                bind : 'context * binder -> 'context}
+               -> 'context -> (Elab.con -> unit)
+    val app : {kind : Elab.kind' -> unit,
+               con : Elab.con' -> unit}
+              -> Elab.con -> unit
     val existsB : {kind : 'context * Elab.kind' -> bool,
                   con : 'context * Elab.con' -> bool,
                    bind : 'context * binder -> 'context}