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

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

24 files changed, 332 insertions, 148 deletions

diff --git a/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh b/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh
new file mode 100644
index 0000000000..3bdbcf7d6e
--- /dev/null
+++ b/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "13312" ] || [ "$CI_BRANCH" = "attributes+bool_single" ]; then
+
+    overlay unicoq https://github.com/ejgallego/unicoq attributes+bool_single
+    overlay elpi https://github.com/ejgallego/coq-elpi attributes+bool_single
+
+fi
diff --git a/doc/changelog/02-specification-language/13312-attributes+bool_single.rst b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst
new file mode 100644
index 0000000000..f069bc616b
--- /dev/null
+++ b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst
@@ -0,0 +1,17 @@
+- **Changed:**
+  :term:`Boolean attributes <boolean attribute>` are now specified using
+  key/value pairs, that is to say :n:`@ident__attr{? = {| yes | no } }`.
+  If the value is missing, the default is :n:`yes`.  The old syntax is still
+  supported, but produces the ``deprecated-attribute-syntax`` warning.
+
+  Deprecated attributes are :attr:`universes(monomorphic)`,
+  :attr:`universes(notemplate)` and :attr:`universes(noncumulative)`, which are
+  respectively replaced by :attr:`universes(polymorphic=no) <universes(polymorphic)>`,
+  :attr:`universes(template=no) <universes(template)>`
+  and :attr:`universes(cumulative=no) <universes(cumulative)>`.
+  Attributes :attr:`program` and :attr:`canonical` are also affected,
+  with the syntax :n:`@ident__attr(false)` being deprecated in favor of
+  :n:`@ident__attr=no`.
+
+  (`#13312 <https://github.com/coq/coq/pull/13312>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 298ea4b4ab..104f84a253 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -99,15 +99,15 @@ coercions.
 
    Enables the program mode, in which 1) typechecking allows subset coercions and
    2) the elaboration of pattern matching of :cmd:`Fixpoint` and
-   :cmd:`Definition` act as if the :attr:`program` attribute had been
+   :cmd:`Definition` acts as if the :attr:`program` attribute has been
    used, generating obligations if there are unresolved holes after
    typechecking.
 
-.. attr:: program
+.. attr:: program{? = {| yes | no } }
    :name: program; Program
 
-   Allows using the Program mode on a specific
-   definition.  An alternative syntax is to use the legacy ``Program``
+   This :term:`boolean attribute` allows using or disabling the Program mode on a specific
+   definition.  An alternative and commonly used syntax is to use the legacy ``Program``
    prefix (cf. :n:`@legacy_attr`) as it is elsewhere in this chapter.
 
 .. _syntactic_control:
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..4615a8dfca 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -122,33 +122,37 @@ in a universe strictly higher than :g:`Set`.
 Polymorphic, Monomorphic
 -------------------------
 
-.. attr:: universes(polymorphic)
-   :name: universes(polymorphic); Polymorphic
+.. attr:: universes(polymorphic{? = {| yes | no } })
+   :name: universes(polymorphic); Polymorphic; Monomorphic
+
+   This :term:`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 ``universes(polymorphic=no)`` is used, 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`).
 
-   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.
+.. attr:: universes(monomorphic)
 
-.. flag:: Universe Polymorphism
+   .. deprecated:: 8.13
 
-   This flag is off by default.  When it is on, new declarations are
-   polymorphic unless the :attr:`universes(monomorphic)` attribute is
-   used.
+      Use :attr:`universes(polymorphic=no) <universes(polymorphic)>`
+      instead.
 
-.. attr:: universes(monomorphic)
-   :name: universes(monomorphic); Monomorphic
+.. flag:: Universe Polymorphism
 
-   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`).
+   This flag is off by default.  When it is on, new declarations are
+   polymorphic unless the :attr:`universes(polymorphic=no) <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.
@@ -171,19 +175,27 @@ Polymorphism` flag is on or the :attr:`universes(polymorphic)` or
 Cumulative, NonCumulative
 -------------------------
 
-.. attr:: universes(cumulative)
-   :name: universes(cumulative); Cumulative
+.. attr:: universes(cumulative{? = {| yes | no } })
+   :name: universes(cumulative); Cumulative; NonCumulative
 
    Polymorphic inductive types, coinductive types, variants and
-   records can be declared cumulative using this attribute or the
-   legacy ``Cumulative`` prefix (see :n:`@legacy_attr`) which, as
+   records can be declared cumulative using this :term:`boolean attribute`
+   or the legacy ``Cumulative`` prefix (see :n:`@legacy_attr`) which, as
    shown in the examples, is more commonly used.
 
    This means that two instances of the same inductive type (family)
    are convertible based on the universe variances; they do not need
    to be equal.
 
-   .. exn:: The cumulative and noncumulative attributes can only be used in a polymorphic context.
+   When the attribtue is off, the inductive type is 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.
+
+   .. exn:: The cumulative attribute can only be used in a polymorphic context.
 
       Using this attribute requires being in a polymorphic context,
       i.e. either having the :flag:`Universe Polymorphism` flag on, or
@@ -192,26 +204,21 @@ Cumulative, NonCumulative
 
    .. note::
 
-      ``#[ universes(polymorphic), universes(cumulative) ]`` can be
-      abbreviated into ``#[ universes(polymorphic, cumulative) ]``.
+      :n:`#[ universes(polymorphic{? = yes }), universes(cumulative{? = {| yes | no } }) ]` can be
+      abbreviated into :n:`#[ universes(polymorphic{? = yes }, cumulative{? = {| yes | no } }) ]`.
 
-.. flag:: Polymorphic Inductive Cumulativity
+.. attr:: universes(noncumulative)
 
-   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.
+   .. deprecated:: 8.13
 
-.. attr:: universes(noncumulative)
-   :name: universes(noncumulative); NonCumulative
+      Use :attr:`universes(cumulative=no) <universes(cumulative)>` instead.
 
-   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`).
+.. flag:: Polymorphic Inductive Cumulativity
 
-   This means that two instances of the same inductive type (family)
-   are convertible only if all the universes are equal.
+   When this flag is on (it is off by default), it makes all
+   subsequent *polymorphic* inductive definitions cumulative, unless
+   the :attr:`universes(cumulative=no) <universes(cumulative)>` attribute is
+   used to override the default.  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..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:
diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst
index 48120503af..f7ce7f1c6c 100644
--- a/doc/sphinx/language/extensions/canonical.rst
+++ b/doc/sphinx/language/extensions/canonical.rst
@@ -87,29 +87,27 @@ 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)
+.. attr:: canonical{? = {| yes | no } }
+   :name: canonical
 
-      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`).
+   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.
 
-      .. example::
+   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`).
 
-         For instance, when declaring the :g:`Setoid` structure above, the
-         :g:`Prf_equiv` field declaration could be written as follows.
-
-         .. 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:`hierarchy_of_structures` for a more realistic example.
 
 .. cmd:: Print Canonical Projections {* @reference }
 
@@ -248,6 +246,8 @@ for each component of the pair. The declaration associates to the key ``*``
 relation ``pair_eq`` whenever the type constructor ``*`` is applied to two
 types being themselves in the ``EQ`` class.
 
+.. _hierarchy_of_structures:
+
 Hierarchy of structures
 ----------------------------
 
@@ -331,7 +331,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} _.
 
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 033ece04de..b5d57f92e9 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -764,6 +764,7 @@ attribute: [
 
 attr_value: [
 | "=" string
+| "=" IDENT
 | "(" attribute_list ")"
 |
 ]
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index dfd3a18908..c9d70a88fc 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -383,6 +383,7 @@ attribute: [
 
 attr_value: [
 | "=" string
+| "=" ident
 | "(" LIST0 attribute SEP "," ")"
 ]
 
diff --git a/test-suite/output/attributes.out b/test-suite/output/attributes.out
new file mode 100644
index 0000000000..25572ee2aa
--- /dev/null
+++ b/test-suite/output/attributes.out
@@ -0,0 +1,11 @@
+The command has indeed failed with message:
+Attribute for canonical specified twice.
+The command has indeed failed with message:
+key 'polymorphic' has been already set.
+The command has indeed failed with message:
+Invalid value 'foo' for key polymorphic
+use one of {yes, no}
+The command has indeed failed with message:
+Invalid syntax polymorphic(foo), try polymorphic={yes, no} instead.
+The command has indeed failed with message:
+Invalid syntax polymorphic(foo, bar), try polymorphic={yes, no} instead.
diff --git a/test-suite/output/attributes.v b/test-suite/output/attributes.v
new file mode 100644
index 0000000000..aef05e6cd4
--- /dev/null
+++ b/test-suite/output/attributes.v
@@ -0,0 +1,9 @@
+Fail #[canonical=yes, canonical=no] Definition a := 3.
+
+Fail #[universes(polymorphic=yes,polymorphic=no)] Definition a := 3.
+
+Fail #[universes(polymorphic=foo)] Definition a := 3.
+
+Fail #[universes(polymorphic(foo))] Definition a := 3.
+
+Fail #[universes(polymorphic(foo,bar))] Definition a := 3.
diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v
index 656362b8fc..d11ae20b8d 100644
--- a/test-suite/success/Template.v
+++ b/test-suite/success/Template.v
@@ -37,7 +37,7 @@ Module Yes.
 End Yes.
 
 Module No.
-  #[universes(notemplate)]
+  #[universes(template=no)]
   Inductive Box (A:Type) : Type := box : A -> Box A.
 
   About Box.
diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v
index b403fc120c..b866c4b074 100644
--- a/test-suite/success/attribute_syntax.v
+++ b/test-suite/success/attribute_syntax.v
@@ -16,11 +16,16 @@ Definition ι T (x: T) := x.
 
 Check ι _ ι.
 
+#[universes(polymorphic=no)]
+Definition ιι T (x: T) := x.
+
+Fail Check ιι _ ιι.
+
 #[program]
 Fixpoint f (n: nat) {wf lt n} : nat := _.
 Reset f.
 
-#[program(true)]
+#[program=yes]
 Fixpoint f (n: nat) {wf lt n} : nat := _.
 Reset f.
 
@@ -43,3 +48,14 @@ Export Set Foo.
 
 Fail #[ export ] Export Foo.
 (* Attribute for Locality specified twice *)
+
+(* Tests for deprecated attribute syntax *)
+Set Warnings "-deprecated-attribute-syntax".
+
+#[program(true)]
+Fixpoint f (n: nat) {wf lt n} : nat := _.
+Reset f.
+
+#[universes(monomorphic)]
+Definition ιιι T (x: T) := x.
+Fail Check ιιι _ ιιι.
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index efba6d332a..fdaeedef8c 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -11,13 +11,29 @@
 open CErrors
 
 (** The type of parsing attribute data *)
+type vernac_flag_type =
+  | FlagIdent of string
+  | FlagString of string
+
 type vernac_flags = vernac_flag list
 and vernac_flag = string * vernac_flag_value
 and vernac_flag_value =
   | VernacFlagEmpty
-  | VernacFlagLeaf of string
+  | VernacFlagLeaf of vernac_flag_type
   | VernacFlagList of vernac_flags
 
+let pr_vernac_flag_leaf = function
+  | FlagIdent b -> Pp.str b
+  | FlagString s -> Pp.(quote (str s))
+
+let rec pr_vernac_flag_value = let open Pp in function
+  | VernacFlagEmpty -> mt ()
+  | VernacFlagLeaf l -> str "=" ++ pr_vernac_flag_leaf l
+  | VernacFlagList s -> surround (prlist_with_sep pr_comma pr_vernac_flag s)
+and pr_vernac_flag (s, arguments) =
+  let open Pp in
+  str s ++ (pr_vernac_flag_value arguments)
+
 let warn_unsupported_attributes =
   CWarnings.create ~name:"unsupported-attributes" ~category:"parsing" ~default:CWarnings.AsError
     (fun atts ->
@@ -105,16 +121,82 @@ let single_key_parser ~name ~key v prev args =
   assert_once ~name prev;
   v
 
-let bool_attribute ~name ~on ~off : bool option attribute =
-  attribute_of_list [(on, single_key_parser ~name ~key:on true);
-               (off, single_key_parser ~name ~key:off false)]
+let pr_possible_values ~values =
+  Pp.(str "{" ++ prlist_with_sep pr_comma str (List.map fst values) ++ str "}")
+
+(** [key_value_attribute ~key ~default ~values] parses a attribute [key=value]
+  with possible [key] [value] in [values], [default] is for compatibility for users
+  doing [qualif(key)] which is parsed as [qualif(key=default)] *)
+let key_value_attribute ~key ~default ~(values : (string * 'a) list) : 'a option attribute =
+  let parser = function
+    | Some v ->
+      CErrors.user_err Pp.(str "key '" ++ str key ++ str "' has been already set.")
+    | None ->
+      begin function
+        | VernacFlagLeaf (FlagIdent b) ->
+          begin match CList.assoc_f String.equal b values with
+            | exception Not_found ->
+              CErrors.user_err
+                Pp.(str "Invalid value '" ++ str b ++ str "' for key " ++ str key ++ fnl () ++
+                    str "use one of " ++ pr_possible_values ~values)
+            | value -> value
+          end
+        | VernacFlagEmpty ->
+          default
+        | err ->
+          CErrors.user_err
+            Pp.(str "Invalid syntax " ++ pr_vernac_flag (key, err) ++ str ", try "
+                ++ str key ++ str "=" ++ pr_possible_values ~values ++ str " instead.")
+      end
+  in
+  attribute_of_list [key, parser]
+
+let bool_attribute ~name : bool option attribute =
+  let values = ["yes", true; "no", false] in
+  key_value_attribute ~key:name ~default:true ~values
+
+let legacy_bool_attribute ~name ~on ~off : bool option attribute =
+  attribute_of_list
+    [(on, single_key_parser ~name ~key:on true);
+     (off, single_key_parser ~name ~key:off false)]
+
+(* important note: we use on as the default for the new bool_attribute ! *)
+let deprecated_bool_attribute_warning =
+  CWarnings.create
+    ~name:"deprecated-attribute-syntax"
+    ~category:"parsing"
+    ~default:CWarnings.Enabled
+    (fun name ->
+       Pp.(str "Syntax for switching off boolean attributes has been updated, use " ++ str name ++ str "=no instead."))
+
+let deprecated_bool_attribute ~name ~on ~off : bool option attribute =
+  bool_attribute ~name:on ++ legacy_bool_attribute ~name ~on ~off |> map (function
+      | None, None ->
+        None
+      | None, Some v ->
+        deprecated_bool_attribute_warning name;
+        Some v
+      | Some v, None -> Some v
+      | Some v1, Some v2 ->
+        CErrors.user_err
+          Pp.(str "attribute " ++ str name ++
+              str ": cannot specify legacy and modern syntax at the same time.")
+    )
 
 (* Variant of the [bool] attribute with only two values (bool has three). *)
 let get_bool_value ~key ~default =
   function
   | VernacFlagEmpty -> default
-  | VernacFlagList [ "true", VernacFlagEmpty ] -> true
-  | VernacFlagList [ "false", VernacFlagEmpty ] -> false
+  | VernacFlagList [ "true", VernacFlagEmpty ] ->
+    deprecated_bool_attribute_warning key;
+    true
+  | VernacFlagList [ "false", VernacFlagEmpty ] ->
+    deprecated_bool_attribute_warning key;
+    false
+  | VernacFlagLeaf (FlagIdent "yes") ->
+    true
+  | VernacFlagLeaf (FlagIdent "no") ->
+    false
   | _ -> user_err Pp.(str "Attribute " ++ str key ++ str " only accepts boolean values.")
 
 let enable_attribute ~key ~default : bool attribute =
@@ -161,18 +243,37 @@ let () = let open Goptions in
 let program =
   enable_attribute ~key:"program" ~default:(fun () -> !program_mode)
 
-let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global"
-
-let option_locality =
+(* This is a bit complex as the grammar in g_vernac.mlg doesn't
+   distingish between the boolean and ternary case.*)
+let option_locality_parser =
   let name = "Locality" in
   attribute_of_list [
-    ("local", single_key_parser ~name ~key:"local" Goptions.OptLocal);
-    ("global", single_key_parser ~name ~key:"global" Goptions.OptGlobal);
-    ("export", single_key_parser ~name ~key:"export" Goptions.OptExport);
-  ] >>= function
+    ("local", single_key_parser ~name ~key:"local" Goptions.OptLocal)
+  ; ("global", single_key_parser ~name ~key:"global" Goptions.OptGlobal)
+  ; ("export", single_key_parser ~name ~key:"export" Goptions.OptExport)
+  ]
+
+let option_locality =
+  option_locality_parser >>= function
   | None -> return Goptions.OptDefault
   | Some l -> return l
 
+(* locality is supposed to be true when local, false when global *)
+let locality =
+  let locality_to_bool =
+    function
+    | Goptions.OptLocal ->
+      true
+    | Goptions.OptGlobal ->
+      false
+    | Goptions.OptExport ->
+      CErrors.user_err Pp.(str "export attribute not supported here")
+    | Goptions.OptDefault ->
+      CErrors.user_err Pp.(str "default attribute not supported here")
+  in
+  option_locality_parser >>= function l ->
+    return (Option.map locality_to_bool l)
+
 let ukey = "universes"
 
 let universe_polymorphism_option_name = ["Universe"; "Polymorphism"]
@@ -188,12 +289,17 @@ let is_universe_polymorphism =
   fun () -> !b
 
 let polymorphic_base =
-  bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic" >>= function
+  deprecated_bool_attribute
+    ~name:"Polymorphism"
+    ~on:"polymorphic" ~off:"monomorphic" >>= function
   | Some b -> return b
   | None -> return (is_universe_polymorphism())
 
 let template =
-  qualify_attribute ukey (bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate")
+  qualify_attribute ukey
+    (deprecated_bool_attribute
+       ~name:"Template"
+       ~on:"template" ~off:"notemplate")
 
 let polymorphic =
   qualify_attribute ukey polymorphic_base
@@ -201,12 +307,12 @@ let polymorphic =
 let deprecation_parser : Deprecation.t key_parser = fun orig args ->
   assert_once ~name:"deprecation" orig;
   match args with
-  | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ]
-  | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] ->
+  | VernacFlagList [ "since", VernacFlagLeaf (FlagString since) ; "note", VernacFlagLeaf (FlagString note) ]
+  | VernacFlagList [ "note", VernacFlagLeaf (FlagString note) ; "since", VernacFlagLeaf (FlagString since) ] ->
     Deprecation.make ~since ~note ()
-  | VernacFlagList [ "since", VernacFlagLeaf since ] ->
+  | VernacFlagList [ "since", VernacFlagLeaf (FlagString since) ] ->
     Deprecation.make ~since ()
-  | VernacFlagList [ "note", VernacFlagLeaf note ] ->
+  | VernacFlagList [ "note", VernacFlagLeaf (FlagString note) ] ->
     Deprecation.make ~note ()
   |  _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
 
@@ -218,7 +324,7 @@ let only_polymorphism atts = parse polymorphic atts
 
 
 let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty]
-let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty]
+let vernac_monomorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagLeaf (FlagIdent "no")]
 
 let canonical_field =
   enable_attribute ~key:"canonical" ~default:(fun () -> true)
@@ -228,7 +334,7 @@ let canonical_instance =
 let uses_parser : string key_parser = fun orig args ->
   assert_once ~name:"using" orig;
   match args with
-  | VernacFlagLeaf str -> str
+  | VernacFlagLeaf (FlagString str) -> str
   |  _ -> CErrors.user_err (Pp.str "Ill formed \"using\" attribute")
 
 let using = attribute_of_list ["using",uses_parser]
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 1969665082..03a14a03ff 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -9,13 +9,19 @@
 (************************************************************************)
 
 (** The type of parsing attribute data *)
+type vernac_flag_type =
+  | FlagIdent of string
+  | FlagString of string
+
 type vernac_flags = vernac_flag list
 and vernac_flag = string * vernac_flag_value
 and vernac_flag_value =
   | VernacFlagEmpty
-  | VernacFlagLeaf of string
+  | VernacFlagLeaf of vernac_flag_type
   | VernacFlagList of vernac_flags
 
+val pr_vernac_flag : vernac_flag -> Pp.t
+
 type +'a attribute
 (** The type of attributes. When parsing attributes if an ['a
    attribute] is present then an ['a] value will be produced.
@@ -82,10 +88,19 @@ val attribute_of_list : (string * 'a key_parser) list -> 'a option attribute
 (** Make an attribute from a list of key parsers together with their
    associated key. *)
 
-val bool_attribute : name:string -> on:string -> off:string -> bool option attribute
-(** Define boolean attribute [name] with value [true] when [on] is
-   provided and [false] when [off] is provided. The attribute may only
-   be set once for a command. *)
+(** Define boolean attribute [name], of the form [name={yes,no}]. The
+   attribute may only be set once for a command. *)
+val bool_attribute : name:string -> bool option attribute
+
+val deprecated_bool_attribute
+  : name:string
+  -> on:string
+  -> off:string
+  -> bool option attribute
+(** Define boolean attribute [name] with will be set when [on] is
+   provided and unset when [off] is provided. The attribute may only
+   be set once for a command; this attribute both accepts the old [on]
+   [off] syntax and new attribute syntax [on=yes] [on=no] *)
 
 val qualify_attribute : string -> 'a attribute -> 'a attribute
 (** [qualified_attribute qual att] treats [#[qual(atts)]] like [att]
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 1aff76114b..116cfc6413 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -119,7 +119,8 @@ GRAMMAR EXTEND Gram
     ]
   ;
   attr_value:
-    [ [ "=" ; v = string -> { VernacFlagLeaf v }
+    [ [ "=" ; v = string -> { VernacFlagLeaf (FlagString v) }
+      | "=" ; v = IDENT -> { VernacFlagLeaf (FlagIdent v) }
       | "(" ; a = attribute_list ; ")" -> { VernacFlagList a }
       | -> { VernacFlagEmpty } ]
     ]
@@ -136,7 +137,7 @@ GRAMMAR EXTEND Gram
       | IDENT "Cumulative" ->
         { ("universes", VernacFlagList ["cumulative", VernacFlagEmpty]) }
       | IDENT "NonCumulative" ->
-        { ("universes", VernacFlagList ["noncumulative", VernacFlagEmpty]) }
+        { ("universes", VernacFlagList ["cumulative", VernacFlagLeaf (FlagIdent "no")]) }
       | IDENT "Private" ->
         { ("private", VernacFlagList ["matching", VernacFlagEmpty]) }
       | IDENT "Program" ->
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 442269ebda..4cee4f7a47 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1331,20 +1331,10 @@ let pr_control_flag (p : control_flag) =
 
 let pr_vernac_control flags = Pp.prlist pr_control_flag flags
 
-let rec pr_vernac_flag (k, v) =
-  let k = keyword k in
-  let open Attributes in
-  match v with
-  | VernacFlagEmpty -> k
-  | VernacFlagLeaf v -> k ++ str " = " ++ qs v
-  | VernacFlagList m -> k ++ str "( " ++ pr_vernac_flags m ++ str " )"
-and pr_vernac_flags m =
-  prlist_with_sep (fun () -> str ", ") pr_vernac_flag m
-
 let pr_vernac_attributes =
   function
   | [] -> mt ()
-  | flags ->  str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut ()
+  | flags ->  str "#[" ++ prlist_with_sep pr_comma Attributes.pr_vernac_flag flags ++ str "]" ++ cut ()
 
 let pr_vernac ({v = {control; attrs; expr}} as v) =
   tag_vernac v
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4e52af7959..0f63dfe5ce 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -674,13 +674,19 @@ let is_polymorphic_inductive_cumulativity =
 let polymorphic_cumulative =
   let error_poly_context () =
     user_err
-      Pp.(str "The cumulative and noncumulative attributes can only be used in a polymorphic context.");
+      Pp.(str "The cumulative attribute can only be used in a polymorphic context.");
   in
   let open Attributes in
   let open Notations in
+  (* EJGA: this seems redudant with code in attributes.ml *)
   qualify_attribute "universes"
-    (bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic"
-     ++ bool_attribute ~name:"Cumulativity" ~on:"cumulative" ~off:"noncumulative")
+    (deprecated_bool_attribute
+       ~name:"Polymorphism"
+       ~on:"polymorphic" ~off:"monomorphic"
+     ++
+     deprecated_bool_attribute
+       ~name:"Cumulativity"
+       ~on:"cumulative" ~off:"noncumulative")
   >>= function
   | Some poly, Some cum ->
      (* Case of Polymorphic|Monomorphic Cumulative|NonCumulative Inductive