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

22 files changed, 69 insertions, 36 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
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4dcf287ef..6514ad8be 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1081,8 +1081,8 @@ let sort_fields ~complete loc fields completer =
           let rec build_proj_list projs proj_kinds idx ~acc_first_idx acc =
             match projs with
               | [] -> (idx, acc_first_idx, acc)
-              | (Some name) :: projs ->
-                 let field_glob_ref = ConstRef name in
+              | (Some field_glob_id) :: projs ->
+                 let field_glob_ref = ConstRef field_glob_id in
                  let first_field = eq_gr field_glob_ref first_field_glob_ref in
                  begin match proj_kinds with
                     | [] -> anomaly (Pp.str "Number of projections mismatch")
@@ -1099,7 +1099,7 @@ let sort_fields ~complete loc fields completer =
                          build_proj_list projs proj_kinds idx ~acc_first_idx acc
                        else
                          build_proj_list projs proj_kinds (idx+1) ~acc_first_idx
-                                         ((idx, field_glob_ref) :: acc)
+                                         ((idx, field_glob_id) :: acc)
                  end
               | None :: projs ->
                  if complete then
@@ -1121,7 +1121,7 @@ let sort_fields ~complete loc fields completer =
                  user_err ?loc:(loc_of_reference field_ref) ~hdr:"intern"
                                (str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
                let remaining_projs, (field_index, _) =
-                 let the_proj (idx, glob_ref) = eq_gr field_glob_ref glob_ref in
+                 let the_proj (idx, glob_id) = eq_gr field_glob_ref (ConstRef glob_id) in
                  try CList.extract_first the_proj remaining_projs
                  with Not_found ->
                    user_err ?loc 
@@ -1646,7 +1646,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
        let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
        let fields =
 	 sort_fields ~complete:true loc fs
-	             (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark st),
+	             (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark (st,Anonymous)),
                                                            Misctypes.IntroAnonymous, None))
        in
        begin
@@ -1726,7 +1726,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
            let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
            (match naming with
            | Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id
-           | _ -> Evar_kinds.QuestionMark st)
+           | _ -> Evar_kinds.QuestionMark (st,Anonymous))
         | Some k -> k
         in
         let solve = match solve with
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli
index 470ad2a23..835e94c77 100644
--- a/intf/evar_kinds.mli
+++ b/intf/evar_kinds.mli
@@ -21,7 +21,7 @@ type t =
      * bool (** Force inference *)
   | BinderType of Name.t
   | NamedHole of Id.t (* coming from some ?[id] syntax *)
-  | QuestionMark of obligation_definition_status
+  | QuestionMark of obligation_definition_status * Name.t
   | CasesType of bool (* true = a subterm of the type *)
   | InternalHole
   | TomatchTypeParameter of inductive * int
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index d68139a4b..cba9c1364 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -636,7 +636,7 @@ let subst_var_with_hole occ tid t =
            else
 	     (incr locref;
               CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
-	      GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),
+	      GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),
                      Misctypes.IntroAnonymous, None)))
         else x
     | c -> map_glob_constr_left_to_right substrec c in
@@ -648,13 +648,13 @@ let subst_hole_with_term occ tc t =
   let locref = ref 0 in
   let occref = ref occ in
   let rec substrec = function
-    | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) } ->
+    | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) } ->
         decr occref;
         if Int.equal !occref 0 then tc
         else
 	  (incr locref;
            CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
-	   GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s))
+	   GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s))
     | c -> map_glob_constr_left_to_right substrec c
   in
   substrec t
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
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index fd5eabe64..35fbec5a6 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -254,7 +254,7 @@ open Evar_kinds
 let mkPattern c = snd (Patternops.pattern_of_glob_constr c)
 let mkGApp f args = CAst.make @@ GApp (f, args)
 let mkGHole = CAst.make @@
-  GHole (QuestionMark (Define false), Misctypes.IntroAnonymous, None)
+  GHole (QuestionMark (Define false,Anonymous), Misctypes.IntroAnonymous, None)
 let mkGProd id c1 c2 = CAst.make @@
   GProd (Name (Id.of_string id), Explicit, c1, c2)
 let mkGArrow c1 c2 = CAst.make @@
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index b99d80e95..ba85286dd 100644
--- a/test-suite/.csdp.cache
+++ b/test-suite/.csdp.cache
diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out
index bf1bf2809..8acfed5d0 100644
--- a/test-suite/output/Show.out
+++ b/test-suite/output/Show.out
@@ -1,12 +1,12 @@
-3 subgoals (ID 29)
+3 subgoals (ID 31)
   
   H : 0 = 0
   ============================
   1 = 1
 
-subgoal 2 (ID 33) is:
+subgoal 2 (ID 35) is:
  1 = S (S m')
-subgoal 3 (ID 20) is:
+subgoal 3 (ID 22) is:
  S (S n') = S m
 
 (dependent evars: (printing disabled) )
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index c70467912..d28ee4276 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -6,13 +6,13 @@ fun e : option L => match e with
      : option L -> option L
 fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
      : forall m n p : nat, S m <= S n + p -> m <= n + p
-fun n : nat => let x : T n := A n in ?t ?y : T n
+fun n : nat => let y : T n := A n in ?t ?x : T n
      : forall n : nat, T n
 where
-?t : [n : nat  x := A n : T n |- ?T -> T n] 
-?y : [n : nat  x := A n : T n |- ?T] 
-fun n : nat => ?t ?y : T n
+?t : [n : nat  y := A n : T n |- ?T -> T n] 
+?x : [n : nat  y := A n : T n |- ?T] 
+fun n : nat => ?t ?x : T n
      : forall n : nat, T n
 where
 ?t : [n : nat |- ?T -> T n] 
-?y : [n : nat |- ?T] 
+?x : [n : nat |- ?T] 
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index 1825db167..f761a4dc5 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -27,5 +27,5 @@ Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H).
 (* Note: exact numbers of evars are not important... *)
 
 Inductive T (n:nat) : Type := A : T n.
-Check fun n (x:=A n:T n) => _ _ : T n.
+Check fun n (y:=A n:T n) => _ _ : T n.
 Check fun n => _ _ : T n.
diff --git a/test-suite/output/names.out b/test-suite/output/names.out
index 9471b892d..48be63a46 100644
--- a/test-suite/output/names.out
+++ b/test-suite/output/names.out
@@ -3,3 +3,9 @@ In environment
 y : nat
 The term "a y" has type "{y0 : nat | y = y0}"
 while it is expected to have type "{x : nat | x = y}".
+1 focused subgoal
+(shelved: 1)
+  
+  H : ?n <= 3 -> 3 <= ?n -> ?n = 3
+  ============================
+  True
diff --git a/test-suite/output/names.v b/test-suite/output/names.v
index b3b5071a0..f1efd0df2 100644
--- a/test-suite/output/names.v
+++ b/test-suite/output/names.v
@@ -3,3 +3,7 @@
 
 Parameter a : forall x, {y:nat|x=y}.
 Fail Definition b y : {x:nat|x=y} := a y.
+
+Goal (forall n m, n <= m -> m <= n -> n = m) -> True.
+intro H; epose proof (H _ 3) as H.
+Show.
diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v
index ffd50f6ef..69dc9aca7 100644
--- a/test-suite/success/Abstract.v
+++ b/test-suite/success/Abstract.v
@@ -1,4 +1,3 @@
-
 (* Cf coqbugs #546 *)
 
 Require Import Omega.
diff --git a/vernac/command.ml b/vernac/command.ml
index e2ebb4d7f..25dd724af 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -1062,7 +1062,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
     mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force fix_sub_ref)),
 	  [| argtyp ; wf_rel ;
 	     Evarutil.e_new_evar env evdref
-	       ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
+	       ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof;
 	     prop |])
   in
   let def = Typing.e_solve_evars env evdref def in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index be58c67a9..47ac16f9c 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -221,7 +221,7 @@ let eterm_obligations env name evm fs ?status t ty =
 	 in
 	 let loc, k = evar_source id evm in
 	 let status = match k with
-           | Evar_kinds.QuestionMark o -> o
+           | Evar_kinds.QuestionMark (o,_) -> o
            | _ -> match status with
                  | Some o -> o
                  | None -> Evar_kinds.Define (not (Program.get_proofs_transparency ()))