3 files changed, 80 insertions, 7 deletions
diff --git a/test-suite/bugs/7333.v b/test-suite/bugs/7333.v
new file mode 100644
index 0000000000..fba5b9029d
--- /dev/null
+++ b/test-suite/bugs/7333.v
@@ -0,0 +1,39 @@
+Module Example1.
+
+CoInductive wrap : Type :=
+ | item : unit -> wrap.
+
+Definition extract (t : wrap) : unit :=
+match t with
+| item x => x
+end.
+
+CoFixpoint close u : unit -> wrap :=
+match u with
+| tt => item
+end.
+
+Definition table : wrap := close tt tt.
+
+Eval vm_compute in (extract table).
+Eval vm_compute in (extract table).
+
+End Example1.
+
+Module Example2.
+
+Set Primitive Projections.
+CoInductive wrap : Type :=
+ item { extract : unit }.
+
+CoFixpoint close u : unit -> wrap :=
+match u with
+| tt => item
+end.
+
+Definition table : wrap := close tt tt.
+
+Eval vm_compute in (extract table).
+Eval vm_compute in (extract table).
+
+End Example2.
diff --git a/test-suite/check b/test-suite/check
deleted file mode 100755
index 3d14f6bc03..0000000000
--- a/test-suite/check
+++ /dev/null
@@ -1,7 +0,0 @@
-#!/bin/sh
-
-MAKE="${MAKE:=make}"
-
-${MAKE} clean > /dev/null 2>&1
-${MAKE} all > /dev/null 2>&1
-cat summary.log
diff --git a/test-suite/coqchk/univ.v b/test-suite/coqchk/univ.v
index 19eea94b19..216338615d 100644
--- a/test-suite/coqchk/univ.v
+++ b/test-suite/coqchk/univ.v
@@ -46,3 +46,44 @@ 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.