aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/elab_err.sig
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-12-18 11:29:13 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2011-12-18 11:29:13 -0500
commit4eb93836d04d18f43d8c4360f290a7977d96c468 (patch)
treeef38476a5b0199272d5dc20a65a306b4c7b2a112 /src/elab_err.sig
parent37cf82d0761088c469205b90e35569674707202f (diff)
Add a new scoping check for unification variables, to fix a type inference bug
Diffstat (limited to 'src/elab_err.sig')
-rw-r--r--src/elab_err.sig2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/elab_err.sig b/src/elab_err.sig
index a66cf61f..14133d08 100644
--- a/src/elab_err.sig
+++ b/src/elab_err.sig
@@ -35,6 +35,7 @@ signature ELAB_ERR = sig
datatype kunify_error =
KOccursCheckFailed of Elab.kind * Elab.kind
| KIncompatible of Elab.kind * Elab.kind
+ | KScope of Elab.kind * Elab.kind
val kunifyError : ElabEnv.env -> kunify_error -> unit
@@ -59,6 +60,7 @@ signature ELAB_ERR = sig
| TooLifty of ErrorMsg.span * ErrorMsg.span
| TooUnify of Elab.con * Elab.con
| TooDeep
+ | CScope of Elab.con * Elab.con
val cunifyError : ElabEnv.env -> cunify_error -> unit