Fix glob_sort_family for SProp

Fixes #12529

1 files changed, 21 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).