5 files changed, 168 insertions, 0 deletions
diff --git a/test-suite/coqchk/bug_7539.v b/test-suite/coqchk/bug_7539.v
new file mode 100644
index 00000000..74ebe929
--- /dev/null
+++ b/test-suite/coqchk/bug_7539.v
@@ -0,0 +1,26 @@
+Set Primitive Projections.
+
+CoInductive Stream : Type := Cons { tl : Stream }.
+
+Fixpoint Str_nth_tl (n:nat) (s:Stream) : Stream :=
+  match n with
+  | O => s
+  | S m => Str_nth_tl m (tl s)
+  end.
+
+CoInductive EqSt (s1 s2: Stream) : Prop := eqst {
+  eqst_tl : EqSt (tl s1) (tl s2);
+}.
+
+Axiom EqSt_reflex : forall (s : Stream), EqSt s s.
+
+CoFixpoint map (s:Stream) : Stream := Cons (map (tl s)).
+
+Lemma Str_nth_tl_map : forall n s, EqSt (Str_nth_tl n (map s)) (map (Str_nth_tl n s)).
+Proof.
+induction n.
++ intros; apply EqSt_reflex.
++ cbn; intros s; apply IHn.
+Qed.
+
+Definition boom : forall s, tl (map s) = map (tl s) := fun s => eq_refl.
diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v
new file mode 100644
index 00000000..03468405
--- /dev/null
+++ b/test-suite/coqchk/cumulativity.v
@@ -0,0 +1,67 @@
+Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
+Set Printing Universes.
+
+Inductive List (A: Type) := nil | cons : A -> List A -> List A.
+
+Section ListLift.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x.
+
+End ListLift.
+
+Lemma LiftL_Lem A (l : List A) : l = LiftL l.
+Proof. reflexivity. Qed.
+
+Section ListLower.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x.
+
+End ListLower.
+
+Lemma LowerL_Lem@{i j|j<i+} (A : Type@{j}) (l : List@{i} A) : l = LowerL@{j i} l.
+Proof. reflexivity. Qed.
+(*
+I disable these tests because cqochk can't process them when compiled with
+   ocaml-4.02.3+32bit and camlp5-4.16 which is the case for Travis!
+
+   I have added this file (including the commented parts below) in
+   test-suite/success/cumulativity.v which doesn't run coqchk on them.
+*)
+(* Inductive Tp := tp : Type -> Tp. *)
+
+(* Section TpLift. *)
+(*   Universe i j. *)
+
+(*   Constraint i < j. *)
+
+(*   Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x. *)
+
+(* End TpLift. *)
+
+(* Lemma LiftC_Lem (t : Tp) : LiftTp t = t. *)
+(* Proof. reflexivity. Qed. *)
+
+(* Section TpLower. *)
+(*   Universe i j. *)
+
+(*   Constraint i < j. *)
+
+(*   Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x. *)
+
+(* End TpLower. *)
+
+
+(* Section subtyping_test. *)
+(*   Universe i j. *)
+(*   Constraint i < j. *)
+
+(*   Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2. *)
+
+(* End subtyping_test. *)
diff --git a/test-suite/coqchk/include.v b/test-suite/coqchk/include.v
new file mode 100644
index 00000000..6232c1b8
--- /dev/null
+++ b/test-suite/coqchk/include.v
@@ -0,0 +1,11 @@
+(* See https://github.com/coq/coq/issues/5747 *)
+Module Type S.
+End S.
+
+Module N.
+Inductive I := .
+End N.
+
+Module M : S.
+  Include N.
+End M.
diff --git a/test-suite/coqchk/primproj2.v b/test-suite/coqchk/primproj2.v
new file mode 100644
index 00000000..f73c627e
--- /dev/null
+++ b/test-suite/coqchk/primproj2.v
@@ -0,0 +1,10 @@
+Set Primitive Projections.
+
+Record Pack (A : Type) := pack { unpack : A }.
+
+Definition p : Pack bool.
+Proof.
+refine (pack _ true).
+Qed.
+
+Definition boom : unpack bool p = let u := unpack _ in u p := eq_refl.
diff --git a/test-suite/coqchk/univ.v b/test-suite/coqchk/univ.v
index 84a4009d..21633861 100644
--- a/test-suite/coqchk/univ.v
+++ b/test-suite/coqchk/univ.v
@@ -33,3 +33,57 @@ Inductive finite_of_order T (D : T -> Type) (n : natural) :=
     (rank_injective : injective_in T natural D rank)
     (rank_onto :
        forall i, equivalent (less_than i n) (in_image T natural D rank i)).
+
+(* Constraints *)
+Universes i j.
+Inductive constraint1 : (Type -> Type) -> Type := mk_constraint1 : constraint1 (fun x : Type@{i} => (x : Type@{j})).
+Constraint i < j.
+Inductive constraint2 : Type@{j} := mkc2 (_ : Type@{i}).
+Universes i' j'.
+Constraint i' = j'.
+Inductive constraint3 : (Type -> Type) -> Type := mk_constraint3 : constraint3 (fun x : Type@{i'} => (x : Type@{j'})).
+Inductive constraint4 : (Type -> Type) -> Type
+  := mk_constraint4 : let U1 := Type in
+                      let U2 := Type in
+                      constraint4 (fun x : U1 => (x : U2)).
+
+Module CMP_CON.
+  (* Comparison of opaque constants MUST be up to the universe graph.
+     See #6798. *)
+  Universe big.
+
+  Polymorphic Lemma foo@{u} : Type@{big}.
+  Proof. exact Type@{u}. Qed.
+
+  Universes U V.
+
+  Definition yo : foo@{U} = foo@{V} := eq_refl.
+End CMP_CON.
+
+Set Universe Polymorphism.
+
+Module POLY_SUBTYP.
+
+  Module Type T.
+    Axiom foo : Type.
+    Parameter bar@{u v|u = v} : foo@{u}.
+  End T.
+
+  Module M.
+    Axiom foo : Type.
+    Axiom bar@{u v|u = v} : foo@{v}.
+  End M.
+
+  Module F (A:T). End F.
+
+  Module X := F M.
+
+End POLY_SUBTYP.
+
+Module POLY_IND.
+
+  Polymorphic Inductive ind@{u v | u < v} : Prop := .
+
+  Polymorphic Definition cst@{u v | v < u} := Prop.
+
+End POLY_IND.