3 files changed, 102 insertions, 0 deletions
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index 8f95484cfd..356a67efec 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -87,3 +87,41 @@ Check fun (x : E) => match x with c => e c end.
 Inductive C' : bool -> Set := c' : C' true.
 Inductive E' (b : bool) : Set := e' :> C' b -> E' b.
 Check fun (x : E' true) => match x with c' => e' true c' end.
+
+(* Check use of the no-dependency strategy when a type constraint is
+   given (and when the "inversion-and-dependencies-as-evars" strategy
+   is not strong enough because of a constructor with a type whose
+   pattern structure is not refined enough for it to be captured by
+   the inversion predicate) *)
+
+Inductive K : bool -> bool -> Type := F : K true true | G x : K x x.
+
+Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
+        match y with
+        | F  => f y H1
+        | G _ => f y H2
+        end : Q y z.
+
+(* Check use of the maximal-dependency-in-variable strategy even when
+   no explicit type constraint is given (and when the
+   "inversion-and-dependencies-as-evars" strategy is not strong enough
+   because of a constructor with a type whose pattern structure is not
+   refined enough for it to be captured by the inversion predicate) *)
+
+Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
+        match y with
+        | F  => f y true H1
+        | G b => f y b H2
+        end.
+
+(* Check use of the maximal-dependency-in-variable strategy for "Var"
+   variables *)
+
+Goal forall z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z), Q y z.
+intros z P Q y H1 H2 f.
+Show.
+refine (match y with
+        | F  => f y true H1
+        | G b => f y b H2
+        end).
+Qed.
diff --git a/test-suite/success/CombinedScheme.v b/test-suite/success/CombinedScheme.v
new file mode 100644
index 0000000000..d6ca7a299f
--- /dev/null
+++ b/test-suite/success/CombinedScheme.v
@@ -0,0 +1,35 @@
+Inductive even (x : bool) : nat -> Type :=
+| evenO : even x 0
+| evenS : forall n, odd x n -> even x (S n)
+with odd (x : bool) : nat -> Type :=
+| oddS : forall n, even x n -> odd x (S n).
+
+Scheme even_ind_prop := Induction for even Sort Prop
+with odd_ind_prop := Induction for odd Sort Prop.
+
+Combined Scheme even_cprop from even_ind_prop, odd_ind_prop.
+
+Check even_cprop :
+  forall (x : bool) (P : forall n : nat, even x n -> Prop)
+    (P0 : forall n : nat, odd x n -> Prop),
+    P 0 (evenO x) ->
+    (forall (n : nat) (o : odd x n), P0 n o -> P (S n) (evenS x n o)) ->
+    (forall (n : nat) (e : even x n), P n e -> P0 (S n) (oddS x n e)) ->
+    (forall (n : nat) (e : even x n), P n e) /\
+    (forall (n : nat) (o : odd x n), P0 n o).
+
+Scheme even_ind_type := Induction for even Sort Type
+with odd_ind_type := Induction for odd Sort Type.
+
+(* This didn't work in v8.7 *)
+
+Combined Scheme even_ctype from even_ind_type, odd_ind_type.
+
+Check even_ctype :
+  forall (x : bool) (P : forall n : nat, even x n -> Prop)
+    (P0 : forall n : nat, odd x n -> Prop),
+    P 0 (evenO x) ->
+    (forall (n : nat) (o : odd x n), P0 n o -> P (S n) (evenS x n o)) ->
+    (forall (n : nat) (e : even x n), P n e -> P0 (S n) (oddS x n e)) ->
+    (forall (n : nat) (e : even x n), P n e) *
+    (forall (n : nat) (o : odd x n), P0 n o).
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.