2 files changed, 77 insertions, 0 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/bugs/closed/bug_12532.v b/test-suite/bugs/closed/bug_12532.v
new file mode 100644
index 0000000000..665f6643e6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12532.v
@@ -0,0 +1,56 @@
+(** This is a change of behaviour introduced by PR #12532. It is not clear
+    whether it is a legit behaviour but it is worth having it in the test
+    suite. *)
+
+Module Foo.
+
+Axiom whatever : Type.
+Axiom name : Type.
+Axiom nw : forall (P : Type), name -> P.
+Axiom raft_data : Type.
+Axiom In : raft_data -> Prop.
+
+Axiom foo : forall st st', In st -> In st'.
+
+Definition params := prod whatever raft_data.
+
+Goal forall
+  (d : raft_data),
+  (forall (h : name), In (@snd whatever raft_data (@nw params h))) ->
+  In d.
+Proof.
+intros.
+eapply foo.
+solve [debug eauto].
+Abort.
+
+End Foo.
+
+Module Bar.
+
+Axiom whatever : Type.
+Axiom AppendEntries : whatever -> Prop.
+Axiom name : Type.
+Axiom nw : forall (P : Type), name -> P.
+Axiom raft_data : Type.
+Axiom In : raft_data -> Prop.
+
+Axiom foo :
+  forall st st' lid,
+    (AppendEntries lid -> In st) -> AppendEntries lid -> In st'.
+
+Definition params := prod whatever raft_data.
+
+Goal forall
+  (d : raft_data),
+  (forall (h : name) (w : whatever),
+    AppendEntries w -> In (@snd whatever raft_data (@nw params h))) ->
+  In d.
+Proof.
+intros.
+eapply foo.
+intros.
+solve [debug eauto].
+Abort.
+
+End Bar.