Merge PR #8509: Fix numerous anomalies with Scheme Equality

3 files changed, 43 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4612.v b/test-suite/bugs/closed/4612.v
new file mode 100644
index 0000000000..ce95f26acc
--- /dev/null
+++ b/test-suite/bugs/closed/4612.v
@@ -0,0 +1,7 @@
+(* While waiting for support, check at least that it does not raise an anomaly *)
+
+Inductive ctype :=
+| Struct: list ctype -> ctype
+| Bot : ctype.
+
+Fail Scheme Equality for ctype.
diff --git a/test-suite/bugs/closed/4859.v b/test-suite/bugs/closed/4859.v
new file mode 100644
index 0000000000..7be0bedcfc
--- /dev/null
+++ b/test-suite/bugs/closed/4859.v
@@ -0,0 +1,7 @@
+(* Not supported but check at least that it does not raise an anomaly *)
+
+Inductive Fin{n : nat} : Set :=
+| F1{i : nat}{e : n = S i}
+| FS{i : nat}(f : @ Fin i){e : n = S i}.
+
+Fail Scheme Equality for Fin.
diff --git a/test-suite/success/SchemeEquality.v b/test-suite/success/SchemeEquality.v
new file mode 100644
index 0000000000..85d5c3e123
--- /dev/null
+++ b/test-suite/success/SchemeEquality.v
@@ -0,0 +1,29 @@
+(* Examples of use of Scheme Equality *)
+
+Module A.
+Definition N := nat.
+Inductive list := nil | cons : N -> list -> list.
+Scheme Equality for list.
+End A.
+
+Module B.
+  Section A.
+    Context A (eq_A:A->A->bool)
+            (A_bl : forall x y, eq_A x y = true -> x = y)
+            (A_lb : forall x y, x = y -> eq_A x y = true).
+    Inductive I := C : A -> I.
+    Scheme Equality for I.
+  End A.
+End B.
+
+Module C.
+  Parameter A : Type.
+  Parameter eq_A : A->A->bool.
+  Parameter A_bl : forall x y, eq_A x y = true -> x = y.
+  Parameter A_lb : forall x y, x = y -> eq_A x y = true.
+  Hint Resolve A_bl A_lb : core.
+  Inductive I := C : A -> I.
+  Scheme Equality for I.
+  Inductive J := D : list A -> J.
+  Scheme Equality for J.
+End C.