Merge PR #12434: Slight improvement in naming dependent existential variables in goals

Reviewed-by: SkySkimmer

4 files changed, 59 insertions, 9 deletions

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.