aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretype_errors.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pretype_errors.mli')
-rw-r--r--pretyping/pretype_errors.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 51103ca194..a0d459fe6b 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -59,6 +59,7 @@ type pretype_error =
| NonLinearUnification of Name.t * constr
(** Pretyping *)
| VarNotFound of Id.t
+ | EvarNotFound of Id.t
| UnexpectedType of constr * constr
| NotProduct of constr
| TypingError of type_error
@@ -155,6 +156,8 @@ val error_not_product :
val error_var_not_found : ?loc:Loc.t -> env -> Evd.evar_map -> Id.t -> 'b
+val error_evar_not_found : ?loc:Loc.t -> env -> Evd.evar_map -> Id.t -> 'b
+
(** {6 Typeclass errors } *)
val unsatisfiable_constraints : env -> Evd.evar_map -> Evar.t option ->