aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language/core/basic.rst
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-11-18 22:00:25 +0000
committerGitHub2020-11-18 22:00:25 +0000
commit7ebdf6bdbca2be4fc4ecddff0ac97bbb41c80cd0 (patch)
treeb12b82d14a9249a671b27e84caf12cda999531c6 /doc/sphinx/language/core/basic.rst
parentfea83b040f285e4316fd9d63d4c940d9fe444d91 (diff)
parentefa6673158f5eaa3fc11c0b3d1e3285c4acc129a (diff)
Merge PR #13312: [attributes] Allow boolean, single-value attributes.
Reviewed-by: Zimmi48 Reviewed-by: SkySkimmer Ack-by: gares
Diffstat (limited to 'doc/sphinx/language/core/basic.rst')
-rw-r--r--doc/sphinx/language/core/basic.rst26
1 files changed, 14 insertions, 12 deletions
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 5406da38a1..2b262b89c0 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -369,6 +369,7 @@ this attribute`.
attributes ::= {* #[ {*, @attribute } ] } {* @legacy_attr }
attribute ::= @ident {? @attr_value }
attr_value ::= = @string
+ | = @ident
| ( {*, @attribute } )
legacy_attr ::= {| Local | Global }
| {| Polymorphic | Monomorphic }
@@ -379,21 +380,22 @@ this attribute`.
The order of top-level attributes doesn't affect their meaning. ``#[foo,bar]``, ``#[bar,foo]``,
``#[foo]#[bar]`` and ``#[bar]#[foo]`` are equivalent.
+:gdef:`Boolean attributes <boolean attribute>` take the form :n:`@ident__attr{? = {| yes | no } }`.
+When the :n:`{| yes | no }` value is omitted, the default is :n:`yes`.
+
The legacy attributes (:n:`@legacy_attr`) provide an older, alternate syntax
for certain attributes. They are equivalent to new attributes as follows:
-================ ================================
-Legacy attribute New attribute
-================ ================================
-`Local` :attr:`local`
-`Global` :attr:`global`
-`Polymorphic` :attr:`universes(polymorphic)`
-`Monomorphic` :attr:`universes(monomorphic)`
-`Cumulative` :attr:`universes(cumulative)`
-`NonCumulative` :attr:`universes(noncumulative)`
-`Private` :attr:`private(matching)`
-`Program` :attr:`program`
-================ ================================
+============================= ================================
+Legacy attribute New attribute
+============================= ================================
+`Local` :attr:`local`
+`Global` :attr:`global`
+`Polymorphic`, `Monomorphic` :attr:`universes(polymorphic)`
+`Cumulative`, `NonCumulative` :attr:`universes(cumulative)`
+`Private` :attr:`private(matching)`
+`Program` :attr:`program`
+============================= ================================
Attributes appear in the HTML documentation in blue or gray boxes
after the label "Attribute". In the pdf, they appear after the