Adding a new evar source to remember the name of evars which were

named in the original term.

Useful at least for debugging, useful to give a better message than
"this placeholder", even if in the loc is known in this case.

5 files changed, 10 insertions, 4 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index bffb40727..7006fde3c 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1299,6 +1299,7 @@ let pr_decl (decl,ok) =
                            print_constr c ++ str (if ok then ")" else "}")
 
 let pr_evar_source = function
+  | Evar_kinds.NamedHole id -> pr_id id
   | Evar_kinds.QuestionMark _ -> str "underscore"
   | Evar_kinds.CasesType false -> str "pattern-matching return predicate"
   | Evar_kinds.CasesType true ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 235e6e24f..c102d8e11 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1739,7 +1739,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
         let k = match k with
         | None ->
            let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
-           Evar_kinds.QuestionMark st
+           (match naming with
+           | Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id
+           | _ -> Evar_kinds.QuestionMark st)
         | Some k -> k
         in
         let solve = match solve with
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli
index afc5e3bab..470ad2a23 100644
--- a/intf/evar_kinds.mli
+++ b/intf/evar_kinds.mli
@@ -20,6 +20,7 @@ type t =
   | ImplicitArg of global_reference * (int * Id.t option)
      * bool (** Force inference *)
   | BinderType of Name.t
+  | NamedHole of Id.t (* coming from some ?[id] syntax *)
   | QuestionMark of obligation_definition_status
   | CasesType of bool (* true = a subterm of the type *)
   | InternalHole
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 468446982..95341307a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -275,9 +275,9 @@ let rec find_row_ind = function
 let inductive_template evdref env tmloc ind =
   let indu = evd_comb1 (Evd.fresh_inductive_instance env) evdref ind in
   let arsign = inductive_alldecls_env env indu in
-  let hole_source = match tmloc with
-    | Some loc -> fun i -> (loc, Evar_kinds.TomatchTypeParameter (ind,i))
-    | None -> fun _ -> (Loc.ghost, Evar_kinds.InternalHole) in
+  let hole_source i = match tmloc with
+    | Some loc -> (loc, Evar_kinds.TomatchTypeParameter (ind,i))
+    | None -> (Loc.ghost, Evar_kinds.TomatchTypeParameter (ind,i)) in
    let (_,evarl,_) =
     List.fold_right
       (fun decl (subst,evarl,n) ->
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 891662b93..6cff805fc 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -532,6 +532,8 @@ let pr_trailing_ne_context_of env sigma =
   else (str " in environment:"++ pr_context_unlimited env sigma)
 
 let rec explain_evar_kind env sigma evk ty = function
+  | Evar_kinds.NamedHole id ->
+      strbrk "the existential variable named " ++ pr_id id
   | Evar_kinds.QuestionMark _ ->
       strbrk "this placeholder of type " ++ ty
   | Evar_kinds.CasesType false ->