Slight improvement in naming existential variables.

In a Meta := Evar unification problem and the Meta is bound to a
(named) binder, and the Evar is a GoalEvar, we set the source of the
evar to be the one of the Meta.

5 files changed, 81 insertions, 18 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index ff13676818..f0ee8ae68f 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1174,12 +1174,34 @@ let meta_declare mv v ?(name=Anonymous) evd =
   let metas = Metamap.add mv (Cltyp(name,mk_freelisted v)) evd.metas in
   set_metas evd metas
 
+(* If the meta is defined then forget its name *)
+let meta_name evd mv =
+  try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous
+
+let evar_source_of_meta mv evd =
+  match meta_name evd mv with
+  | Anonymous -> Loc.tag Evar_kinds.GoalEvar
+  | Name id   -> Loc.tag @@ Evar_kinds.VarInstance id
+
+let use_meta_source evd mv v =
+  match Constr.kind v with
+  | Evar (evk,_) ->
+    let f = function
+    | None -> None
+    | Some evi as x ->
+      match evi.evar_source with
+      | None, Evar_kinds.GoalEvar -> Some { evi with evar_source = evar_source_of_meta mv evd }
+      | _ -> x in
+    { evd with undf_evars = EvMap.update evk f evd.undf_evars }
+  | _ -> evd
+
 let meta_assign mv (v, pb) evd =
   let modify _ = function
   | Cltyp (na, ty) -> Clval (na, (mk_freelisted v, pb), ty)
   | _ -> anomaly ~label:"meta_assign" (Pp.str "already defined.")
   in
   let metas = Metamap.modify mv modify evd.metas in
+  let evd = use_meta_source evd mv v in
   set_metas evd metas
 
 let meta_reassign mv (v, pb) evd =
@@ -1190,10 +1212,6 @@ let meta_reassign mv (v, pb) evd =
   let metas = Metamap.modify mv modify evd.metas in
   set_metas evd metas
 
-(* If the meta is defined then forget its name *)
-let meta_name evd mv =
-  try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous
-
 let clear_metas evd = {evd with metas = Metamap.empty}
 
 let meta_merge ?(with_univs = true) evd1 evd2 =
@@ -1217,11 +1235,6 @@ let retract_coercible_metas evd =
   let metas = Metamap.Smart.mapi map evd.metas in
   !mc, set_metas evd metas
 
-let evar_source_of_meta mv evd =
-  match meta_name evd mv with
-  | Anonymous -> Loc.tag Evar_kinds.GoalEvar
-  | Name id   -> Loc.tag @@ Evar_kinds.VarInstance id
-
 let dependent_evar_ident ev evd =
   let evi = find evd ev in
   match evi.evar_source with
diff --git a/test-suite/output-coqtop/DependentEvars.out b/test-suite/output-coqtop/DependentEvars.out
index 9ca3fa3357..2e69b94505 100644
--- a/test-suite/output-coqtop/DependentEvars.out
+++ b/test-suite/output-coqtop/DependentEvars.out
@@ -77,14 +77,14 @@ p14 < 3 focused subgoals
   p123 : (P1 -> P2) -> P3
   p34 : P3 -> P4
   ============================
-  ?P -> (?Goal2 -> P4) /\ ?Goal2
+  ?P -> (?P0 -> P4) /\ ?P0
 
 subgoal 2 is:
- ?P -> (?Goal2 -> P4) /\ ?Goal2
+ ?P -> (?P0 -> P4) /\ ?P0
 subgoal 3 is:
  ?P
 
-(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11)
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal: ?X4 ?X5 ?X10 ?X11)
 
 p14 < 
 Coq < 
diff --git a/test-suite/output-coqtop/DependentEvars2.out b/test-suite/output-coqtop/DependentEvars2.out
index 29ebba7c86..63bfafa88d 100644
--- a/test-suite/output-coqtop/DependentEvars2.out
+++ b/test-suite/output-coqtop/DependentEvars2.out
@@ -90,13 +90,13 @@ Try unfocusing with "}".
 (shelved: 2)
 
 subgoal 1 is:
- ?P -> (?Goal2 -> P4) /\ ?Goal2
+ ?P -> (?P0 -> P4) /\ ?P0
 subgoal 2 is:
- ?P -> (?Goal2 -> P4) /\ ?Goal2
+ ?P -> (?P0 -> P4) /\ ?P0
 subgoal 3 is:
  ?P
 
-(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal:)
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal:)
 
 p14 < 3 focused subgoals
 (shelved: 2)
@@ -106,14 +106,14 @@ p14 < 3 focused subgoals
   p123 : (P1 -> P2) -> P3
   p34 : P3 -> P4
   ============================
-  ?P -> (?Goal2 -> P4) /\ ?Goal2
+  ?P -> (?P0 -> P4) /\ ?P0
 
 subgoal 2 is:
- ?P -> (?Goal2 -> P4) /\ ?Goal2
+ ?P -> (?P0 -> P4) /\ ?P0
 subgoal 3 is:
  ?P
 
-(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11)
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal: ?X4 ?X5 ?X10 ?X11)
 
 p14 < 
 Coq < 
diff --git a/test-suite/output/unification.out b/test-suite/output/unification.out
index dfd755da61..cf31871e5a 100644
--- a/test-suite/output/unification.out
+++ b/test-suite/output/unification.out
@@ -9,3 +9,27 @@ Unable to unify "T" with "?X@{x0:=x; x:=C a}" (cannot instantiate
 The command has indeed failed with message:
 The term "id" has type "ID" while it is expected to have type 
 "Type -> ?T" (cannot instantiate "?T" because "A" is not in its scope).
+1 focused subgoal
+(shelved: 1)
+  
+  H : forall x : nat, S (S (S x)) = x
+  ============================
+  ?x = 0
+1 focused subgoal
+(shelved: 1)
+  
+  H : forall x : nat, S (S (S x)) = x
+  ============================
+  ?x = 0
+1 focused subgoal
+(shelved: 1)
+  
+  H : forall x : nat, S (S (S x)) = x
+  ============================
+  ?x = 0
+1 focused subgoal
+(shelved: 1)
+  
+  H : forall x : nat, S x = x
+  ============================
+  ?y = 0
diff --git a/test-suite/output/unification.v b/test-suite/output/unification.v
index ff99f2e23c..fe7366a97d 100644
--- a/test-suite/output/unification.v
+++ b/test-suite/output/unification.v
@@ -10,3 +10,29 @@ Fail Check fun x => match x return ?[X] with C a => a end.
 Fail Check (id:Type -> _).
 
 End A.
+
+(* Choice of evar names *)
+
+Goal (forall x, S (S (S x)) = x) -> exists x, S x = 0.
+eexists.
+rewrite H.
+Show.
+Undo 2.
+eexists ?[x].
+rewrite H.
+Show.
+Undo 2.
+eexists ?[y].
+rewrite H.
+Show.
+reflexivity.
+Qed.
+
+(* Preserve the name if there is one *)
+
+Goal (forall x, S x = x) -> exists x, S x = 0.
+eexists ?[y].
+rewrite H.
+Show.
+reflexivity.
+Qed.