Add a new scoping check for unification variables, to fix a type inference bug

1 files changed, 7 insertions, 0 deletions

diff --git a/src/elab_util.sig b/src/elab_util.sig
index 2998e7db..8a013554 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -64,6 +64,13 @@ structure Con : sig
     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}