Merge PR #9144: Fixes #4633: clearer message unknown existential

Ack-by: herbelin
Reviewed-by: ppedrot

4 files changed, 9 insertions, 3 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 517834f014..c7cc2dbc8a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -739,7 +739,7 @@ and detype_r d flags avoid env sigma t =
       let id,l =
         try
           let id = match Evd.evar_ident evk sigma with
-          | None -> Termops.pr_evar_suggested_name evk sigma
+          | None -> Termops.evar_suggested_name evk sigma
           | Some id -> id
           in
           let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in
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 =
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 ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ace2868255..c23b20a5d3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -486,8 +486,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
       let id = interp_ltac_id env id in
       let evk =
         try Evd.evar_key id sigma
-        with Not_found ->
-          user_err ?loc  (str "Unknown existential variable.") in
+        with Not_found -> error_evar_not_found ?loc !!env sigma id in
       let hyps = evar_filtered_context (Evd.find sigma evk) in
       let sigma, args = pretype_instance k0 resolve_tc env sigma loc hyps evk inst in
       let c = mkEvar (evk, args) in