Support for using type information to infer more precise evar sources.

This allows a better control on the name to give to an evar and, in
particular, to address the issue about naming produced by "epose
proof" in one of the comment of Zimmi48 at PR #248 (see file names.v).

Incidentally updating output of Show output test (evar numbers shifted).

6 files changed, 13 insertions, 5 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 6cba6f607..3ef725cbb 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -367,10 +367,10 @@ let push_rel_context_to_named_context env sigma typ =
 
 let default_source = Loc.tag @@ Evar_kinds.InternalHole
 
-let restrict_evar evd evk filter candidates =
+let restrict_evar evd evk filter ?src candidates =
   let evd = Sigma.to_evar_map evd in
   let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in
-  let evd, evk' = Evd.restrict evk filter ?candidates evd in
+  let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in
   Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd)
 
 let new_pure_evar_full evd evi =
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index fcc435a2e..496ec5bc4 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -57,7 +57,7 @@ val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma
 val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
 
 val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t ->
-  constr list option -> (existential_key, 'r) Sigma.sigma
+  ?src:Evar_kinds.t Loc.located -> constr list option -> (existential_key, 'r) Sigma.sigma
 
 (** Polymorphic constants *)
 
diff --git a/engine/evd.ml b/engine/evd.ml
index b677705bc..48fceae9e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -653,12 +653,13 @@ let define evk body evd =
   let evar_names = EvNames.remove_name_defined evk evd.evar_names in
   { evd with defn_evars; undf_evars; last_mods; evar_names }
 
-let restrict evk filter ?candidates evd =
+let restrict evk filter ?candidates ?src evd =
   let evk' = new_untyped_evar () in
   let evar_info = EvMap.find evk evd.undf_evars in
   let evar_info' =
     { evar_info with evar_filter = filter;
       evar_candidates = candidates;
+      evar_source = (match src with None -> evar_info.evar_source | Some src -> src);
       evar_extra = Store.empty } in
   let last_mods = match evd.conv_pbs with
   | [] ->  evd.last_mods
diff --git a/engine/evd.mli b/engine/evd.mli
index 005332470..86755c360 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -240,7 +240,7 @@ val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool ->
 (** {6 Misc} *)
 
 val restrict : evar -> Filter.t -> ?candidates:constr list ->
-  evar_map -> evar_map * evar
+  ?src:Evar_kinds.t located -> evar_map -> evar_map * evar
 (** Restrict an undefined evar into a new evar by filtering context and
     possibly limiting the instances to a set of candidates *)
 
diff --git a/engine/proofview.ml b/engine/proofview.ml
index ddfc0e39d..29bb1ef39 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -696,6 +696,12 @@ let mark_in_evm ~goal evd content =
   let info =
     if goal then
       { info with Evd.evar_source = match info.Evd.evar_source with
+            (* Two kinds for goal evars:
+               - GoalEvar (morally not dependent)
+               - VarInstance (morally dependent of some name).
+               This is a heuristic for naming these evars. *)
+            | loc, (Evar_kinds.QuestionMark (_,Names.Name id) |
+                    Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id
             | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
             | loc,_ -> loc,Evar_kinds.GoalEvar }
     else info
diff --git a/engine/termops.ml b/engine/termops.ml
index ca32c06a7..1ec2b8103 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -112,6 +112,7 @@ let pr_evar_suggested_name evk sigma =
   | None -> match evi.evar_source with
   | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
   | _,Evar_kinds.VarInstance id -> id
+  | _,Evar_kinds.QuestionMark (_,Name id) -> id
   | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
   | _ ->
       let env = reset_with_named_context evi.evar_hyps (Global.env()) in