From 30d0b1052b6351a539558ff1fe16e4f8578c03ba Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 5 Dec 2018 19:46:26 +0100
Subject: Fixes #4633: more explicit error message when referring to a
 generated evar.

---
 pretyping/pretype_errors.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'pretyping/pretype_errors.mli')

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 ->
-- 
cgit v1.2.3