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.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'pretyping/pretype_errors.ml')

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 01b0d96f98..dc6607557d 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -53,6 +53,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
@@ -167,6 +168,9 @@ let error_not_product ?loc env sigma c =
 let error_var_not_found ?loc env sigma s =
   raise_pretype_error ?loc (env, sigma, VarNotFound s)
 
+let error_evar_not_found ?loc env sigma id =
+  raise_pretype_error ?loc (env, sigma, EvarNotFound id)
+
 (*s Typeclass errors *)
 
 let unsatisfiable_constraints env evd ev comp =
-- 
cgit v1.2.3