Fixes #4633: more explicit error message when referring to a generated evar.

4 files changed, 24 insertions, 2 deletions

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
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index a2b5c8d70a..3342f0e0fd 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -599,6 +599,20 @@ let explain_var_not_found env id =
   spc () ++ str "was not found" ++
   spc () ++ str "in the current" ++ spc () ++ str "environment" ++ str "."
 
+
+let explain_evar_not_found env sigma id =
+  let undef = Evar.Map.domain (Evd.undefined_map sigma) in
+  let all_undef_evars = Evar.Set.elements undef in
+  let f ev = Id.equal id (Termops.evar_suggested_name ev sigma) in
+  if List.exists f all_undef_evars then
+    (* The name is used for printing but is not user-given *)
+    str "?" ++ Id.print id ++
+    strbrk " is a generated name. Only user-given names for existential variables" ++
+    strbrk " can be referenced. To give a user name to an existential variable," ++
+    strbrk " introduce it with the ?[name] syntax."
+  else
+    str "Unknown existential variable."
+
 let explain_wrong_case_info env (ind,u) ci =
   let pi = pr_inductive env ind in
   if eq_ind ci.ci_ind ind then
@@ -813,6 +827,7 @@ let explain_pretype_error env sigma err =
   | UnifOccurCheck (ev,rhs) -> explain_occur_check env sigma ev rhs
   | UnsolvableImplicit (evk,exp) -> explain_unsolvable_implicit env sigma evk exp
   | VarNotFound id -> explain_var_not_found env id
+  | EvarNotFound id -> explain_evar_not_found env sigma id
   | UnexpectedType (actual,expect) ->
     let env, actual, expect = contract2 env sigma actual expect in
     explain_unexpected_type env sigma actual expect
@@ -834,6 +849,7 @@ let explain_pretype_error env sigma err =
   | TypingError t -> explain_type_error env sigma t
   | CannotUnifyOccurrences (b,c1,c2,e) -> explain_cannot_unify_occurrences env sigma b c1 c2 e
   | UnsatisfiableConstraints (c,comp) -> explain_unsatisfiable_constraints env sigma c comp
+
 (* Module errors *)
 
 open Modops