From 697bfeba6f5bdff48b254092a3f7f6616080e9b2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 19 Sep 2018 13:42:44 +0200
Subject: Allow successive attributes #[foo] #[bar]

---
 doc/sphinx/language/gallina-specification-language.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc')

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