2 files changed, 31 insertions, 0 deletions
diff --git a/test-suite/modules/SeveralWith.v b/test-suite/modules/SeveralWith.v
new file mode 100644
index 0000000000..bbf72a7648
--- /dev/null
+++ b/test-suite/modules/SeveralWith.v
@@ -0,0 +1,12 @@
+Module Type S.
+Parameter A : Type.
+End S.
+
+Module Type ES.
+Parameter A : Type.
+Parameter eq : A -> A -> Type.
+End ES.
+
+Module Make
+  (AX : S)
+  (X : ES with Definition A := AX.A with Definition eq := @eq AX.A).
diff --git a/test-suite/modules/cumpoly.v b/test-suite/modules/cumpoly.v
new file mode 100644
index 0000000000..654b86cb44
--- /dev/null
+++ b/test-suite/modules/cumpoly.v
@@ -0,0 +1,19 @@
+Set Universe Polymorphism.
+
+(** Check that variance subtyping is respected. The signature T is asking for
+    invariance, while M provide an irrelevant implementation, which is deemed
+    legit.
+
+    There is currently no way to go the other way around, so it's not possible
+    to generate a counter-example that should fail with the wrong subtyping.
+*)
+
+Module Type T.
+Parameter t@{i|Set <= i} : Type@{i}.
+Cumulative Inductive I@{i|Set <= i} : Type@{i} := C : t@{i} -> I.
+End T.
+
+Module M : T.
+Definition t@{i|Set <= i} : Type@{i} := nat.
+Cumulative Inductive I@{i|Set <= i} : Type@{i} := C : t@{i} -> I.
+End M.