Merge PR #8515: Command driven attributes

3 files changed, 36 insertions, 5 deletions

diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v
index 1c6e2d81d8..cfc25c3346 100644
--- a/test-suite/success/Template.v
+++ b/test-suite/success/Template.v
@@ -25,7 +25,7 @@ Module AutoNo.
 End AutoNo.
 
 Module Yes.
-  #[template]
+  #[universes(template)]
   Inductive Box@{i} (A:Type@{i}) : Type@{i} := box : A -> Box A.
 
   About Box.
@@ -37,7 +37,7 @@ Module Yes.
 End Yes.
 
 Module No.
-  #[notemplate]
+  #[universes(notemplate)]
   Inductive Box (A:Type) : Type := box : A -> Box A.
 
   About Box.
diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v
index 7b972f4ed9..f4f59a3c16 100644
--- a/test-suite/success/attribute_syntax.v
+++ b/test-suite/success/attribute_syntax.v
@@ -11,7 +11,7 @@ End Scope.
 
 Fail Check 0 = true :> nat.
 
-#[polymorphic]
+#[universes(polymorphic)]
 Definition ι T (x: T) := x.
 
 Check ι _ ι.
@@ -24,9 +24,9 @@ Reset f.
 Ltac foo := foo.
 
 Module M.
-  #[local] #[polymorphic] Definition zed := Type.
+  #[local] #[universes(polymorphic)] Definition zed := Type.
 
-  #[local, polymorphic] Definition kats := Type.
+  #[local, universes(polymorphic)] Definition kats := Type.
 End M.
 Check M.zed@{_}.
 Fail Check zed.
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.