From 0e225553a2ee1c39e0f070edb6528d109dd878ac Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 19 Sep 2018 22:23:39 +0200
Subject: Fixing #4612 (anomaly with Scheme called on unsupported inductive
 type).

We raise a normal error instead of an anomaly.

This fixes also #2550, #8492.

Note in passing: While the case of a type "Inductive I := list I -> I"
is difficult, the case of a "Inductive I := list nat -> I" should be
easily doable.
---
 test-suite/bugs/closed/4612.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/4612.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3


From 82a3fb5d5c0d0c5660effec59f3800ee5e8a125d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 19 Sep 2018 22:47:36 +0200
Subject: Fixing #4859 (anomaly with Scheme called on inductive type with
 indices).

We raise a normal error instead of an anomaly.
---
 test-suite/bugs/closed/4859.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/4859.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3


From f30996a89a31a1a54ab481f752e5febb8a8ac0ed Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 20 Sep 2018 12:59:28 +0200
Subject: Fixing a typo in a comment.

---
 test-suite/success/SchemeEquality.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/success/SchemeEquality.v

(limited to 'test-suite')

diff --git a/test-suite/success/SchemeEquality.v b/test-suite/success/SchemeEquality.v
new file mode 100644
index 0000000000..00e84bff38
--- /dev/null
+++ b/test-suite/success/SchemeEquality.v
@@ -0,0 +1,7 @@
+(* Examples of use of Scheme Equality *)
+
+Module A.
+Definition N := nat.
+Inductive list := nil | cons : N -> list -> list.
+Scheme Equality for list.
+End A.
-- 
cgit v1.2.3


From 9afe18c3190bb0210e03bf40f3af101a7c5604da Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 20 Sep 2018 13:32:08 +0200
Subject: Scheme Equality: support for working in a context of Parameters.

It was working in very specific context of section variables. We make
it work similarly in the same kind of specific context of
Parameters. See test file SchemeEquality.v for the expected form. See
discussion at PR #8509.
---
 test-suite/success/SchemeEquality.v | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/SchemeEquality.v b/test-suite/success/SchemeEquality.v
index 00e84bff38..85d5c3e123 100644
--- a/test-suite/success/SchemeEquality.v
+++ b/test-suite/success/SchemeEquality.v
@@ -5,3 +5,25 @@ 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.
-- 
cgit v1.2.3