diff options
| author | Vincent Laporte | 2018-09-26 13:39:36 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-09-26 13:39:36 +0000 |
| commit | 8c3f395e52020f82822100730026a950c3653c8c (patch) | |
| tree | 1d5d6997eb9ace3857d12fabaaa21a3de3250102 /doc/sphinx/language | |
| parent | 3f486b2334fa3a5ab7774e212a5c592ba241535c (diff) | |
| parent | 697bfeba6f5bdff48b254092a3f7f6616080e9b2 (diff) | |
Merge PR #8504: Allow successive attributes #[foo] #[bar]
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 4 |
1 files changed, 2 insertions, 2 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), |