Allow successive attributes #[foo] #[bar]

3 files changed, 16 insertions, 7 deletions

diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index daf34500bf..593afa8f20 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -522,7 +522,7 @@ The Vernacular
 ==============
 
 .. productionlist:: coq
-   decorated-sentence : [`decoration`] `sentence`
+   decorated-sentence : [ `decoration` … `decoration` ] `sentence`
    sentence           : `assumption`
                       : | `definition`
                       : | `inductive`
@@ -1438,7 +1438,7 @@ Attributes
 
 Any vernacular command can be decorated with a list of attributes, enclosed
 between ``#[`` (hash and opening square bracket) and ``]`` (closing square bracket)
-and separated by commas ``,``.
+and separated by commas ``,``. Multiple space-separated blocks may be provided.
 
 Each attribute has a name (an identifier) and may have a value.
 A value is either a :token:`string` (in which case it is specified with an equal ``=`` sign),
diff --git a/test-suite/success/attribute-syntax.v b/test-suite/success/attribute-syntax.v
index 83fb3d0c8e..241d4eb200 100644
--- a/test-suite/success/attribute-syntax.v
+++ b/test-suite/success/attribute-syntax.v
@@ -1,4 +1,4 @@
-From Coq Require Program.
+From Coq Require Program.Wf.
 
 Section Scope.
 
@@ -21,3 +21,13 @@ Fixpoint f (n: nat) {wf lt n} : nat := _.
 
 #[deprecated(since="8.9.0")]
 Ltac foo := foo.
+
+Module M.
+  #[local] #[polymorphic] Definition zed := Type.
+
+  #[local, polymorphic] Definition kats := Type.
+End M.
+Check M.zed@{_}.
+Fail Check zed.
+Check M.kats@{_}.
+Fail Check kats.
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 650b28ea67..7dd5471f3f 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -83,11 +83,10 @@ GRAMMAR EXTEND Gram
     ]
   ;
   decorated_vernac:
-    [ [ a = attributes ; fv = vernac -> { let (f, v) = fv in (List.append a f, v) }
-      | fv = vernac -> { fv } ]
-    ]
+    [ [ a = LIST0 quoted_attributes ; fv = vernac ->
+        { let (f, v) = fv in (List.append (List.flatten a) f, v) } ] ]
   ;
-  attributes:
+  quoted_attributes:
     [ [ "#[" ; a = attribute_list ; "]" -> { a } ]
     ]
   ;