1 files changed, 33 insertions, 0 deletions
diff --git a/test-suite/coqchk/univ.v b/test-suite/coqchk/univ.v
index 19eea94b19..43815b61ea 100644
--- a/test-suite/coqchk/univ.v
+++ b/test-suite/coqchk/univ.v
@@ -46,3 +46,36 @@ 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.