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

Ack-by: herbelin
Reviewed-by: ppedrot

8 files changed, 29 insertions, 7 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index 137770d8f0..3e902129f3 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -38,7 +38,7 @@ let set_print_constr f = term_printer := f
 
 module EvMap = Evar.Map
 
-let pr_evar_suggested_name evk sigma =
+let evar_suggested_name evk sigma =
   let open Evd in
   let base_id evk' evi =
   match evar_ident evk' sigma with
@@ -67,7 +67,7 @@ let pr_existential_key sigma evk =
 let open Evd in
 match evar_ident evk sigma with
 | None ->
-  str "?" ++ Id.print (pr_evar_suggested_name evk sigma)
+  str "?" ++ Id.print (evar_suggested_name evk sigma)
 | Some id ->
   str "?" ++ Id.print id
 
diff --git a/engine/termops.mli b/engine/termops.mli
index 7920af8e0e..61a6ec1cd6 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -304,7 +304,7 @@ open Evd
 
 val pr_existential_key : evar_map -> Evar.t -> Pp.t
 
-val pr_evar_suggested_name : Evar.t -> evar_map -> Id.t
+val evar_suggested_name : Evar.t -> evar_map -> Id.t
 
 val pr_evar_info : env -> evar_map -> evar_info -> Pp.t
 val pr_evar_constraints : evar_map -> evar_constraint list -> Pp.t
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
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index c1ea067567..878e9f477b 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -546,7 +546,7 @@ let to_constr p =
 
 module GoalMap = Evar.Map
 
-let goal_to_evar g sigma = Id.to_string (Termops.pr_evar_suggested_name g sigma)
+let goal_to_evar g sigma = Id.to_string (Termops.evar_suggested_name g sigma)
 
 open Goal.Set
 
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index ebbec86b9c..f78b43e2fa 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -598,6 +598,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
@@ -812,6 +826,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
@@ -833,6 +848,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