6 files changed, 90 insertions, 10 deletions
diff --git a/test-suite/bugs/closed/bug_12529.v b/test-suite/bugs/closed/bug_12529.v
new file mode 100644
index 0000000000..bc3c9a28bd
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12529.v
@@ -0,0 +1,21 @@
+Goal SProp.
+match goal with |- SProp => idtac end.
+Fail match goal with |- Prop => idtac end.
+Abort.
+
+Goal Prop.
+Fail match goal with |- SProp => idtac end.
+match goal with |- Prop => idtac end.
+Abort.
+
+Class F A := f : A.
+
+Inductive pFalse : Prop  := .
+Inductive sFalse : SProp := .
+
+Hint Extern 0 (F Prop) => exact pFalse : typeclass_instances.
+Definition pf := f : Prop.
+
+Hint Extern 0 (F SProp) => exact sFalse : typeclass_instances.
+Definition sf := (f : SProp).
+Definition pf' := (f : Prop).
diff --git a/test-suite/micromega/zify.v b/test-suite/micromega/zify.v
index 8fd7398638..a12623c3c0 100644
--- a/test-suite/micromega/zify.v
+++ b/test-suite/micromega/zify.v
@@ -159,7 +159,7 @@ Require Import ZifyClasses.
 Require Import ZifyInst.
 
 Instance Zero : CstOp (@zero znat : nat) := Op_O.
-Add CstOp Zero.
+Add Zify CstOp Zero.
 
 
 Goal  @zero znat = 0%nat.
@@ -227,3 +227,12 @@ Goal forall (f : Z -> bool), negb (negb (f 0)) = f 0.
 Proof.
   intros. lia.
 Qed.
+
+Ltac Zify.zify_pre_hook ::= unfold is_true in *.
+
+Goal forall x y : nat, is_true (Nat.eqb x 1) ->
+                       is_true (Nat.eqb y 0) ->
+                       is_true (Nat.eqb (x + y) 1).
+Proof.
+lia.
+Qed.
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.