From cc95e2f89f88a6e37f1d98ce55e479491c40145a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 9 Oct 2018 15:01:38 +0200
Subject: Make attributes more general to make defining #[universes(...)] easy

---
 test-suite/success/Template.v         | 4 ++--
 test-suite/success/attribute_syntax.v | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3