4 files changed, 56 insertions, 0 deletions
diff --git a/test-suite/coqchk/bug_8655.v b/test-suite/coqchk/bug_8655.v
new file mode 100644
index 00000000..06d08b20
--- /dev/null
+++ b/test-suite/coqchk/bug_8655.v
@@ -0,0 +1 @@
+Inductive IND2 (A:Type) (T:=fun _ : Type->Type => A) := CONS2 : IND2 A -> IND2 (T IND2).
diff --git a/test-suite/coqchk/bug_8876.v b/test-suite/coqchk/bug_8876.v
new file mode 100644
index 00000000..2d20511a
--- /dev/null
+++ b/test-suite/coqchk/bug_8876.v
@@ -0,0 +1,19 @@
+(* -*- coq-prog-args: ("-noinit"); -*- *)
+Require Import Coq.Init.Notations.
+
+Notation "x -> y" := (forall _ : x, y).
+
+Inductive eq {A:Type} (a:A) : A -> Prop := eq_refl : eq a a.
+
+Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
+Set Printing Universes.
+
+(* Constructors for an inductive with indices *)
+Module WithIndex.
+  Inductive foo@{i} : (Prop -> Prop) -> Prop := mkfoo: foo (fun x => x).
+
+  Monomorphic Universes i j.
+  Monomorphic Constraint i < j.
+  Definition bar : eq mkfoo@{i} mkfoo@{j} := eq_refl _.
+End WithIndex.
diff --git a/test-suite/coqchk/bug_8881.v b/test-suite/coqchk/bug_8881.v
new file mode 100644
index 00000000..dfc209b3
--- /dev/null
+++ b/test-suite/coqchk/bug_8881.v
@@ -0,0 +1,23 @@
+
+(* Check use of equivalence on inductive types (bug #1242) *)
+
+Module Type ASIG.
+  Inductive t : Set := a | b : t.
+  Definition f := fun x => match x with a => true | b => false end.
+End ASIG.
+
+Module Type BSIG.
+  Declare Module A : ASIG.
+  Definition f := fun x => match x with A.a => true | A.b => false end.
+End BSIG.
+
+Module C (A : ASIG) (B : BSIG with Module A:=A).
+
+  (* Check equivalence is considered in "case_info" *)
+  Lemma test : forall x, A.f x = B.f x.
+  Proof.
+    intro x. unfold B.f, A.f.
+    destruct x; reflexivity.
+  Qed.
+
+End C.
diff --git a/test-suite/coqchk/include_primproj.v b/test-suite/coqchk/include_primproj.v
new file mode 100644
index 00000000..804ba1d3
--- /dev/null
+++ b/test-suite/coqchk/include_primproj.v
@@ -0,0 +1,13 @@
+(* #7329 *)
+Set Primitive Projections.
+
+Module M.
+  Module Bar.
+    Record Box := box { unbox : Type }.
+
+    Axiom foo : Box.
+    Axiom baz : forall _ : unbox foo, unbox foo.
+  End Bar.
+End M.
+
+Include M.