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).

3 files changed, 24 insertions, 8 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c2c8065a9..426157372 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2064,8 +2064,8 @@ let mk_JMeq evdref typ x typ' y =
 let mk_JMeq_refl evdref typ x = 
   papp evdref coq_JMeq_refl [| typ; x |]
 
-let hole = CAst.make @@
-  GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false),
+let hole na = CAst.make @@
+  GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na),
          Misctypes.IntroAnonymous, None)
 
 let constr_of_pat env evdref arsign pat avoid =
@@ -2168,7 +2168,7 @@ let vars_of_ctx sigma ctx =
 	    prev,
 	    (CAst.make @@ GApp (
 		(CAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), 
-		   [hole; CAst.make @@ GVar prev])) :: vars
+		   [hole na; CAst.make @@ GVar prev])) :: vars
 	| _ ->
 	    match RelDecl.get_name decl with
 		Anonymous -> invalid_arg "vars_of_ctx"
@@ -2301,7 +2301,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	       | l  -> CAst.make @@ GApp (bref, l)
 	 in
 	 let branch = match ineqs with
-	     Some _ -> CAst.make @@ GApp (branch, [ hole ])
+	     Some _ -> CAst.make @@ GApp (branch, [ hole Anonymous ])
 	   | None -> branch
 	 in
 	 incr i;
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 3ef17912f..83c26058a 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -90,8 +90,8 @@ let inh_pattern_coerce_to ?loc env pat ind1 ind2 =
 
 open Program
 
-let make_existential ?loc ?(opaque = not (get_proofs_transparency ()))  env evdref c =
-  let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque)) in
+let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c =
+  let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque,na)) in
   Evarutil.e_new_evar env evdref ~src c
 
 let app_opt env evdref f t =
@@ -181,7 +181,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
 		let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in
 		let pred = mkLambda (n, eqT, applist (lift 1 c, args)) in
 		let eq = papp evdref coq_eq_ind [| eqT; hdx; hdy |] in
-		let evar = make_existential ?loc env evdref eq in
+		let evar = make_existential ?loc n env evdref eq in
 		let eq_app x = papp evdref coq_eq_rect
 		  [| eqT; hdx; pred; x; hdy; evar|] 
 		in
@@ -324,7 +324,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
 	    Some
 	      (fun x ->
 		 let cx = app_opt env evdref c x in
-		 let evar = make_existential ?loc env evdref (mkApp (p, [| cx |]))
+		 let evar = make_existential ?loc Anonymous env evdref (mkApp (p, [| cx |]))
 		 in
 		   (papp evdref sig_intro [| u; p; cx; evar |]))
 	| None ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e72394fa2..b0663af70 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -383,6 +383,21 @@ let process_inference_flags flags env initial_sigma (sigma,c) =
   let c = if flags.expand_evars then nf_evar sigma c else c in
   sigma,c
 
+let adjust_evar_source evdref na c =
+  match na, kind !evdref c with
+  | Name id, Evar (evk,args) ->
+     let evi = Evd.find !evdref evk in
+     begin match evi.evar_source with
+     | loc, Evar_kinds.QuestionMark (b,Anonymous) ->
+        let src = (loc,Evar_kinds.QuestionMark (b,na)) in
+        let sigma = Sigma.Unsafe.of_evar_map !evdref in
+        let Sigma (evk', evd, _) = restrict_evar sigma evk (evar_filter evi) ~src None in
+        evdref := Sigma.to_evar_map evd;
+        mkEvar (evk',args)
+     | _ -> c
+     end
+  | _, _ -> c
+
 (* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
 let allow_anonymous_refs = ref false
 
@@ -785,6 +800,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 		  args, nf_evar !evdref (j_val hj)
 		else [], j_val hj
 	    in
+            let ujval = adjust_evar_source evdref na ujval in
 	    let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in
 	    let j = { uj_val = value; uj_type = typ } in
 	      apply_rec env (n+1) j candargs rest