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.

1 files changed, 22 insertions, 0 deletions

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.