4 files changed, 38 insertions, 2 deletions
diff --git a/test-suite/output/attributes.out b/test-suite/output/attributes.out
new file mode 100644
index 0000000000..25572ee2aa
--- /dev/null
+++ b/test-suite/output/attributes.out
@@ -0,0 +1,11 @@
+The command has indeed failed with message:
+Attribute for canonical specified twice.
+The command has indeed failed with message:
+key 'polymorphic' has been already set.
+The command has indeed failed with message:
+Invalid value 'foo' for key polymorphic
+use one of {yes, no}
+The command has indeed failed with message:
+Invalid syntax polymorphic(foo), try polymorphic={yes, no} instead.
+The command has indeed failed with message:
+Invalid syntax polymorphic(foo, bar), try polymorphic={yes, no} instead.
diff --git a/test-suite/output/attributes.v b/test-suite/output/attributes.v
new file mode 100644
index 0000000000..aef05e6cd4
--- /dev/null
+++ b/test-suite/output/attributes.v
@@ -0,0 +1,9 @@
+Fail #[canonical=yes, canonical=no] Definition a := 3.
+
+Fail #[universes(polymorphic=yes,polymorphic=no)] Definition a := 3.
+
+Fail #[universes(polymorphic=foo)] Definition a := 3.
+
+Fail #[universes(polymorphic(foo))] Definition a := 3.
+
+Fail #[universes(polymorphic(foo,bar))] Definition a := 3.
diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v
index 656362b8fc..d11ae20b8d 100644
--- a/test-suite/success/Template.v
+++ b/test-suite/success/Template.v
@@ -37,7 +37,7 @@ Module Yes.
 End Yes.
 
 Module No.
-  #[universes(notemplate)]
+  #[universes(template=no)]
   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 b403fc120c..b866c4b074 100644
--- a/test-suite/success/attribute_syntax.v
+++ b/test-suite/success/attribute_syntax.v
@@ -16,11 +16,16 @@ Definition ι T (x: T) := x.
 
 Check ι _ ι.
 
+#[universes(polymorphic=no)]
+Definition ιι T (x: T) := x.
+
+Fail Check ιι _ ιι.
+
 #[program]
 Fixpoint f (n: nat) {wf lt n} : nat := _.
 Reset f.
 
-#[program(true)]
+#[program=yes]
 Fixpoint f (n: nat) {wf lt n} : nat := _.
 Reset f.
 
@@ -43,3 +48,14 @@ Export Set Foo.
 
 Fail #[ export ] Export Foo.
 (* Attribute for Locality specified twice *)
+
+(* Tests for deprecated attribute syntax *)
+Set Warnings "-deprecated-attribute-syntax".
+
+#[program(true)]
+Fixpoint f (n: nat) {wf lt n} : nat := _.
+Reset f.
+
+#[universes(monomorphic)]
+Definition ιιι T (x: T) := x.
+Fail Check ιιι _ ιιι.