Merge PR#248: Adding eassert, eset, epose, etc.

6 files changed, 13 insertions, 5 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 6cba6f6075..3ef725cbbd 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 fcc435a2ec..496ec5bc43 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 b677705bc9..48fceae9ec 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 0053324706..86755c360b 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 ddfc0e39dd..29bb1ef397 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 ca32c06a75..1ec2b81039 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