summaryrefslogtreecommitdiff
path: root/src/elab_err.sig
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2012-04-21 14:57:00 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2012-04-21 14:57:00 -0400
commitd1898695cba6c924456d7de4d1b700072310f752 (patch)
tree3a57d1a9c42edb747baa7d2207cb097191044abb /src/elab_err.sig
parentf87820a0554612aec1fc2965740febef3695b0bd (diff)
Saving proper environments, to use in displaying nested error messages
Diffstat (limited to 'src/elab_err.sig')
-rw-r--r--src/elab_err.sig20
1 files changed, 10 insertions, 10 deletions
diff --git a/src/elab_err.sig b/src/elab_err.sig
index 14133d08..b5e3d64d 100644
--- a/src/elab_err.sig
+++ b/src/elab_err.sig
@@ -43,7 +43,7 @@ signature ELAB_ERR = sig
UnboundCon of ErrorMsg.span * string
| UnboundDatatype of ErrorMsg.span * string
| UnboundStrInCon of ErrorMsg.span * string
- | WrongKind of Elab.con * Elab.kind * Elab.kind * kunify_error
+ | WrongKind of Elab.con * Elab.kind * Elab.kind * ElabEnv.env * kunify_error
| DuplicateField of ErrorMsg.span * string
| ProjBounds of Elab.con * int
| ProjMismatch of Elab.con * Elab.kind
@@ -51,12 +51,12 @@ signature ELAB_ERR = sig
val conError : ElabEnv.env -> con_error -> unit
datatype cunify_error =
- CKind of Elab.kind * Elab.kind * kunify_error
+ CKind of Elab.kind * Elab.kind * ElabEnv.env * kunify_error
| COccursCheckFailed of Elab.con * Elab.con
| CIncompatible of Elab.con * Elab.con
| CExplicitness of Elab.con * Elab.con
| CKindof of Elab.kind * Elab.con * string
- | CRecordFailure of Elab.con * Elab.con * (Elab.con * Elab.con * Elab.con * cunify_error option) option
+ | CRecordFailure of Elab.con * Elab.con * (Elab.con * Elab.con * Elab.con * (ElabEnv.env * cunify_error) option) option
| TooLifty of ErrorMsg.span * ErrorMsg.span
| TooUnify of Elab.con * Elab.con
| TooDeep
@@ -67,12 +67,12 @@ signature ELAB_ERR = sig
datatype exp_error =
UnboundExp of ErrorMsg.span * string
| UnboundStrInExp of ErrorMsg.span * string
- | Unify of Elab.exp * Elab.con * Elab.con * cunify_error
+ | Unify of Elab.exp * Elab.con * Elab.con * ElabEnv.env * cunify_error
| Unif of string * ErrorMsg.span * Elab.con
| WrongForm of string * Elab.exp * Elab.con
| IncompatibleCons of Elab.con * Elab.con
| DuplicatePatternVariable of ErrorMsg.span * string
- | PatUnify of Elab.pat * Elab.con * Elab.con * cunify_error
+ | PatUnify of Elab.pat * Elab.con * Elab.con * ElabEnv.env * cunify_error
| UnboundConstructor of ErrorMsg.span * string list * string
| PatHasArg of ErrorMsg.span
| PatHasNoArg of ErrorMsg.span
@@ -94,13 +94,13 @@ signature ELAB_ERR = sig
datatype sgn_error =
UnboundSgn of ErrorMsg.span * string
| UnmatchedSgi of ErrorMsg.span * Elab.sgn_item
- | SgiWrongKind of ErrorMsg.span * Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * kunify_error
- | SgiWrongCon of ErrorMsg.span * Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * cunify_error
+ | SgiWrongKind of ErrorMsg.span * Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * ElabEnv.env * kunify_error
+ | SgiWrongCon of ErrorMsg.span * Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * ElabEnv.env * cunify_error
| SgiMismatchedDatatypes of ErrorMsg.span * Elab.sgn_item * Elab.sgn_item
- * (Elab.con * Elab.con * cunify_error) option
+ * (Elab.con * Elab.con * ElabEnv.env * cunify_error) option
| SgnWrongForm of ErrorMsg.span * Elab.sgn * Elab.sgn
| UnWhereable of Elab.sgn * string
- | WhereWrongKind of Elab.kind * Elab.kind * kunify_error
+ | WhereWrongKind of Elab.kind * Elab.kind * ElabEnv.env * kunify_error
| NotIncludable of Elab.sgn
| DuplicateCon of ErrorMsg.span * string
| DuplicateVal of ErrorMsg.span * string
@@ -115,7 +115,7 @@ signature ELAB_ERR = sig
| NotFunctor of Elab.sgn
| FunctorRebind of ErrorMsg.span
| UnOpenable of Elab.sgn
- | NotType of ErrorMsg.span * Elab.kind * (Elab.kind * Elab.kind * kunify_error)
+ | NotType of ErrorMsg.span * Elab.kind * (Elab.kind * Elab.kind * ElabEnv.env * kunify_error)
| DuplicateConstructor of string * ErrorMsg.span
| NotDatatype of ErrorMsg.span