Merge PR #13312: [attributes] Allow boolean, single-value attributes.

Reviewed-by: Zimmi48
Reviewed-by: SkySkimmer
Ack-by: gares

6 files changed, 36 insertions, 37 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
diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst
index 3e2ecdc0f0..43bbc8b40d 100644
--- a/doc/sphinx/language/core/coinductive.rst
+++ b/doc/sphinx/language/core/coinductive.rst
@@ -26,10 +26,8 @@ More information on co-inductive definitions can be found in
    For co-inductive types, the only elimination principle is case analysis.
 
    This command supports the :attr:`universes(polymorphic)`,
-   :attr:`universes(monomorphic)`, :attr:`universes(template)`,
-   :attr:`universes(notemplate)`, :attr:`universes(cumulative)`,
-   :attr:`universes(noncumulative)`, :attr:`private(matching)`
-   and :attr:`using` attributes.
+   :attr:`universes(template)`, :attr:`universes(cumulative)`,
+   :attr:`private(matching)`, and :attr:`using` attributes.
 
 .. example::
 
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 79489c85f6..57771c9036 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -90,7 +90,7 @@ Section :ref:`typing-rules`.
    computation on :n:`@term`.
 
    These commands also support the :attr:`universes(polymorphic)`,
-   :attr:`universes(monomorphic)`, :attr:`program` (see :ref:`program_definition`),
+   :attr:`program` (see :ref:`program_definition`),
    :attr:`canonical` and :attr:`using` attributes.
 
    If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index ad7d6f3963..251b5e4955 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -32,10 +32,8 @@ Inductive types
    proposition).
 
    This command supports the :attr:`universes(polymorphic)`,
-   :attr:`universes(monomorphic)`, :attr:`universes(template)`,
-   :attr:`universes(notemplate)`, :attr:`universes(cumulative)`,
-   :attr:`universes(noncumulative)` and :attr:`private(matching)`
-   attributes.
+   :attr:`universes(template)`, :attr:`universes(cumulative)`, and
+   :attr:`private(matching)` attributes.
 
    Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s.
    The :n:`@ident`\s are simultaneously added to the environment before the types of constructors are checked.
@@ -1058,7 +1056,7 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
    at level :math:`\Type` (without annotations or hiding it behind a
    definition) template polymorphic if possible.
 
-   This can be prevented using the :attr:`universes(notemplate)`
+   This can be prevented using the :attr:`universes(template=no) <universes(template)>`
    attribute.
 
    Template polymorphism and full universe polymorphism (see Chapter
@@ -1077,11 +1075,12 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
    the :attr:`universes(template)` attribute: in this case, the
    warning is not emitted.
 
-.. attr:: universes(template)
+.. attr:: universes(template{? = {| yes | no } })
+   :name: universes(template)
 
-   This attribute can be used to explicitly declare an inductive type
-   as template polymorphic, whether the :flag:`Auto Template
-   Polymorphism` flag is on or off.
+   This :term:`boolean attribute` can be used to explicitly declare an
+   inductive type as template polymorphic, whether the :flag:`Auto
+   Template Polymorphism` flag is on or off.
 
    .. exn:: template and polymorphism not compatible
 
@@ -1094,11 +1093,15 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
       The attribute was used but the inductive definition does not
       satisfy the criterion to be template polymorphic.
 
+   When ``universes(template=no)`` is used, it will prevent an
+   inductive type to be template polymorphic, even if the :flag:`Auto
+   Template Polymorphism` flag is on.
+
 .. attr:: universes(notemplate)
 
-   This attribute can be used to prevent an inductive type to be
-   template polymorphic, even if the :flag:`Auto Template
-   Polymorphism` flag is on.
+   .. deprecated:: 8.13
+
+      Use :attr:`universes(template=no) <universes(template)>` instead.
 
 In practice, the rule **Ind-Family** is used by Coq only when all the
 inductive types of the inductive definition are declared with an arity
diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst
index e6df3ee9f5..7eedbcd59a 100644
--- a/doc/sphinx/language/core/records.rst
+++ b/doc/sphinx/language/core/records.rst
@@ -53,10 +53,8 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
    :cmd:`Record` and :cmd:`Structure` are synonyms.
 
    This command supports the :attr:`universes(polymorphic)`,
-   :attr:`universes(monomorphic)`, :attr:`universes(template)`,
-   :attr:`universes(notemplate)`, :attr:`universes(cumulative)`,
-   :attr:`universes(noncumulative)` and :attr:`private(matching)`
-   attributes.
+   :attr:`universes(template)`, :attr:`universes(cumulative)`, and
+   :attr:`private(matching)` attributes.
 
 More generally, a record may have explicitly defined (a.k.a. manifest)
 fields. For instance, we might have:
diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst
index 645986be9c..6ac6626dbe 100644
--- a/doc/sphinx/language/core/variants.rst
+++ b/doc/sphinx/language/core/variants.rst
@@ -17,10 +17,8 @@ Variants
    this variant, unless the :flag:`Nonrecursive Elimination Schemes` flag is on.
 
    This command supports the :attr:`universes(polymorphic)`,
-   :attr:`universes(monomorphic)`, :attr:`universes(template)`,
-   :attr:`universes(notemplate)`, :attr:`universes(cumulative)`,
-   :attr:`universes(noncumulative)` and :attr:`private(matching)`
-   attributes.
+   :attr:`universes(template)`, :attr:`universes(cumulative)`, and
+   :attr:`private(matching)` attributes.
 
    .. exn:: The @natural th argument of @ident must be @ident in @type.
       :undocumented: