[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.

We introduce a warning so boolean attributes are expected to be of the
form `attr={yes,no}` or just `attr` (for `yes`).

We update the documentation, test-suite, and changelog.

10 files changed, 66 insertions, 83 deletions

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 2474c784b8..22527dc379 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -320,10 +320,9 @@ Summary of the commands
    maintained.
 
    Like any command declaring a record, 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(polymorphic)`, :attr:`universes(template)`,
+   :attr:`universes(cumulative)`, and :attr:`private(matching)`
+   attributes.
 
    .. cmd:: Existing Class @qualid
 
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 064107d088..a2ed23335e 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -125,30 +125,27 @@ Polymorphic, Monomorphic
 .. attr:: universes(polymorphic)
    :name: universes(polymorphic); Polymorphic
 
-   This attribute can be used to declare universe polymorphic
-   definitions and inductive types.  There is also a legacy syntax
-   using the ``Polymorphic`` prefix (see :n:`@legacy_attr`) which, as
-   shown in the examples, is more commonly used.
+   This boolean attribute can be used to control whether universe
+   polymorphism is enabled in the definition of an inductive type.
+   There is also a legacy syntax using the ``Polymorphic`` prefix (see
+   :n:`@legacy_attr`) which, as shown in the examples, is more
+   commonly used.
+
+   When ``polymorphic=no`` is set, global universe constraints
+   are produced, even when the :flag:`Universe Polymorphism` flag is
+   on. There is also a legacy syntax using the ``Monomorphic`` prefix
+   (see :n:`@legacy_attr`).
 
 .. flag:: Universe Polymorphism
 
    This flag is off by default.  When it is on, new declarations are
-   polymorphic unless the :attr:`universes(monomorphic)` attribute is
-   used.
-
-.. attr:: universes(monomorphic)
-   :name: universes(monomorphic); Monomorphic
-
-   This attribute can be used to declare universe monomorphic
-   definitions and inductive types (i.e. global universe constraints
-   are produced), even when the :flag:`Universe Polymorphism` flag is
-   on.  There is also a legacy syntax using the ``Monomorphic`` prefix
-   (see :n:`@legacy_attr`).
+   polymorphic unless the :attr:`universes(polymorphic)` attribute is
+   used to override the default.
 
 Many other commands can be used to declare universe polymorphic or
 monomorphic constants depending on whether the :flag:`Universe
-Polymorphism` flag is on or the :attr:`universes(polymorphic)` or
-:attr:`universes(monomorphic)` attributes are used:
+Polymorphism` flag is on or the :attr:`universes(polymorphic)`
+attribute is used:
 
 - :cmd:`Lemma`, :cmd:`Axiom`, etc. can be used to declare universe
   polymorphic constants.
@@ -183,6 +180,9 @@ Cumulative, NonCumulative
    are convertible based on the universe variances; they do not need
    to be equal.
 
+   This means that two instances of the same inductive type (family)
+   are convertible only if all the universes are equal.
+
    .. exn:: The cumulative and noncumulative attributes can only be used in a polymorphic context.
 
       Using this attribute requires being in a polymorphic context,
@@ -195,23 +195,17 @@ Cumulative, NonCumulative
       ``#[ universes(polymorphic), universes(cumulative) ]`` can be
       abbreviated into ``#[ universes(polymorphic, cumulative) ]``.
 
+   When the attribtue is off, the inductive type as non-cumulative
+   even if the :flag:`Polymorphic Inductive Cumulativity` flag is on.
+   There is also a legacy syntax using the ``NonCumulative`` prefix
+   (see :n:`@legacy_attr`).
+
 .. flag:: Polymorphic Inductive Cumulativity
 
    When this flag is on (it is off by default), it makes all
    subsequent *polymorphic* inductive definitions cumulative, unless
-   the :attr:`universes(noncumulative)` attribute is used.  It has no
-   effect on *monomorphic* inductive definitions.
-
-.. attr:: universes(noncumulative)
-   :name: universes(noncumulative); NonCumulative
-
-   Declares the inductive type as non-cumulative even if the
-   :flag:`Polymorphic Inductive Cumulativity` flag is on.  There is
-   also a legacy syntax using the ``NonCumulative`` prefix (see
-   :n:`@legacy_attr`).
-
-   This means that two instances of the same inductive type (family)
-   are convertible only if all the universes are equal.
+   the :attr:`universes(cumulative)` attribute with setting ``off`` is
+   used.  It has no effect on *monomorphic* inductive definitions.
 
 Consider the examples below.
 
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index de5dbe79cc..4d59fc0513 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -533,8 +533,8 @@ Flags, options and attributes
 - **Removed:**
   Unqualified ``polymorphic``, ``monomorphic``, ``template``,
   ``notemplate`` attributes (they were deprecated since Coq 8.10).
-  Use :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`,
-  :attr:`universes(template)` and :attr:`universes(notemplate)` instead
+  Use :attr:`universes(polymorphic)`, ``universes(monomorphic)``,
+  :attr:`universes(template)` and ``universes(notemplate)`` instead
   (`#11663 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann).
 - **Deprecated:**
   :flag:`Hide Obligations` flag
@@ -545,7 +545,7 @@ Flags, options and attributes
   <https://github.com/coq/coq/pull/11162>`_, by Enrico Tassi).
 - **Added:**
   New attributes supported when defining an inductive type
-  :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and
+  :attr:`universes(cumulative)`, ``universes(noncumulative)`` and
   :attr:`private(matching)`, which correspond to legacy attributes
   ``Cumulative``, ``NonCumulative``, and the previously undocumented
   ``Private`` (`#11665 <https://github.com/coq/coq/pull/11665>`_, by
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 5406da38a1..af5c47dba8 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -379,6 +379,9 @@ this attribute`.
 The order of top-level attributes doesn't affect their meaning.  ``#[foo,bar]``, ``#[bar,foo]``,
 ``#[foo]#[bar]`` and ``#[bar]#[foo]`` are equivalent.
 
+Boolean attributes take the form ``attr={yes,no}``, when the key is
+omitted the default is assumed to be ``yes``.
+
 The legacy attributes (:n:`@legacy_attr`) provide an older, alternate syntax
 for certain attributes.  They are equivalent to new attributes as follows:
 
@@ -388,9 +391,9 @@ Legacy attribute  New attribute
 `Local`           :attr:`local`
 `Global`          :attr:`global`
 `Polymorphic`     :attr:`universes(polymorphic)`
-`Monomorphic`     :attr:`universes(monomorphic)`
+`Monomorphic`     :attr:`universes(polymorphic)`
 `Cumulative`      :attr:`universes(cumulative)`
-`NonCumulative`   :attr:`universes(noncumulative)`
+`NonCumulative`   :attr:`universes(cumulative)`
 `Private`         :attr:`private(matching)`
 `Program`         :attr:`program`
 ================  ================================
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..b9453650eb 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,8 +1056,8 @@ 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)`
-   attribute.
+   This can be prevented using the :attr:`universes(template)`
+   attribute with the ``=no`` setting.
 
    Template polymorphism and full universe polymorphism (see Chapter
    :ref:`polymorphicuniverses`) are incompatible, so if the latter is
@@ -1079,9 +1077,9 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
 
 .. attr:: 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 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 +1092,9 @@ 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.
 
-.. 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.
+   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.
 
 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:
diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst
index 48120503af..ec3e3e8aa6 100644
--- a/doc/sphinx/language/extensions/canonical.rst
+++ b/doc/sphinx/language/extensions/canonical.rst
@@ -87,29 +87,26 @@ in :ref:`canonicalstructures`; here only a simple example is given.
       If a same field occurs in several canonical structures, then
       only the structure declared first as canonical is considered.
 
-   .. attr:: canonical(false)
-
-      To prevent a field from being involved in the inference of
-      canonical instances, its declaration can be annotated with the
-      :attr:`canonical(false)` attribute (cf. the syntax of
-      :n:`@record_field`).
+.. attr:: canonical
 
-      .. example::
+   This boolean attribute can decorate a :cmd:`Definition` or
+   :cmd:`Let` command.  It is equivalent to having a :cmd:`Canonical
+   Structure` declaration just after the command.
 
-         For instance, when declaring the :g:`Setoid` structure above, the
-         :g:`Prf_equiv` field declaration could be written as follows.
+   To prevent a field from being involved in the inference of
+   canonical instances, its declaration can be annotated with
+   ``canonical=no`` (cf. the syntax of :n:`@record_field`).
 
-         .. coqdoc::
+   .. example::
 
-            #[canonical(false)] Prf_equiv : equivalence Carrier Equal
+      For instance, when declaring the :g:`Setoid` structure above, the
+      :g:`Prf_equiv` field declaration could be written as follows.
 
-      See :ref:`canonicalstructures` for a more realistic example.
+      .. coqdoc::
 
-.. attr:: canonical
+         #[canonical=no] Prf_equiv : equivalence Carrier Equal
 
-   This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command.
-   It is equivalent to having a :cmd:`Canonical Structure` declaration just
-   after the command.
+   See :ref:`canonicalstructures` for a more realistic example.
 
 .. cmd:: Print Canonical Projections {* @reference }
 
@@ -331,7 +328,7 @@ We need to define a new class that inherits from both ``EQ`` and ``LE``.
                         LE_class : LE.class T;
                         extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }.
 
-    Structure type := _Pack { obj : Type; #[canonical(false)] class_of : class obj }.
+    Structure type := _Pack { obj : Type; #[canonical=no] class_of : class obj }.
 
     Arguments Mixin {e le} _.