1 files changed, 31 insertions, 0 deletions
diff --git a/test-suite/success/module_with_def_univ_poly.v b/test-suite/success/module_with_def_univ_poly.v
new file mode 100644
index 0000000000..a547be4c46
--- /dev/null
+++ b/test-suite/success/module_with_def_univ_poly.v
@@ -0,0 +1,31 @@
+
+(* When doing Module Foo with Definition bar := ..., bar must be
+   generated with the same polymorphism as Foo.bar. *)
+Module Mono.
+  Unset Universe Polymorphism.
+  Module Type T.
+    Parameter foo : Type.
+  End T.
+
+  Module Type F(A:T). End F.
+
+  Set Universe Polymorphism.
+  Module M : T with Definition foo := Type.
+    Monomorphic Definition foo := Type.
+  End M.
+End Mono.
+
+Module Poly.
+  Set Universe Polymorphism.
+
+  Module Type T.
+    Parameter foo@{i|Set < i} : Type@{i}.
+  End T.
+
+  Module Type F(A:T). End F.
+
+  Unset Universe Polymorphism.
+  Module M : T with Definition foo := Set : Type.
+    Polymorphic Definition foo := Set : Type.
+  End M.
+End Poly.