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.

2 files changed, 50 insertions, 0 deletions

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.