From e0380f347d2ebf61b81760a365eea8c84ad3ada4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 15 Oct 2020 17:39:39 +0200
Subject: [attributes] Allow boolean, single-value attributes.

Following discussion in https://github.com/coq/coq/pull/12586 , we
extend the syntax `val=string` to support also arbitrary values.

In particular we support boolean ones, or arbitrary key-pair lists.

This complements the current form `val="string"`, and makes more sense
in general.

Current syntax for the boolean version is `attr=yes` or `attr=no`, but
we could be more liberal if desired.

The general new guideline is that `foo(vals)` is reserved for
the case where `vals` is a list, whereas `foo=val` is for attributes
that allow a unique assignment.

This commit only introduces the support, next commits will migrate
some attributes to this new syntax and deprecate the old versions.
---
 vernac/attributes.ml    | 93 ++++++++++++++++++++++++++++++++++++++++++-------
 vernac/attributes.mli   | 26 +++++++++++---
 vernac/g_vernac.mlg     |  3 +-
 vernac/ppvernac.ml      | 12 +------
 vernac/vernacentries.ml | 10 ++++--
 5 files changed, 113 insertions(+), 31 deletions(-)

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index efba6d332a..fd4fe3d47d 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,9 +121,54 @@ 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)]
+(** [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_sequence str (List.map fst values)))
+            | value -> value
+          end
+        | VernacFlagEmpty ->
+          default
+        | err ->
+          CErrors.user_err Pp.(str "Invalid syntax " ++ pr_vernac_flag (key, err) ++ str ", try " ++ str key ++ str "=value 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 ~name ~on ~off : bool option attribute =
+  bool_attribute ~name:on ++ legacy_bool_attribute ~name ~on ~off |> map (function
+      | None, None ->
+        None
+      | None, Some v ->
+        (* Will insert deprecation warning *)
+        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 =
@@ -161,7 +222,10 @@ 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 locality =
+  deprecated_bool_attribute
+    ~name:"Locality"
+    ~on:"local" ~off:"global"
 
 let option_locality =
   let name = "Locality" in
@@ -188,12 +252,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 +270,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")
 
@@ -228,7 +297,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..60195fe790 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,20 @@ 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={on,off}]. 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
+   [name(on)] [name(off)] and new attribute syntax, with [on] taken as
+   the key. *)
 
 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..d9b664e243 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 } ]
     ]
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..2edd9d4d11 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -678,9 +678,15 @@ let polymorphic_cumulative =
   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
-- 
cgit v1.2.3


From c609c05cf4a5a2a36ca46a0ea890c954d0ae2a5b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 12 Nov 2020 20:21:36 +0100
Subject: [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.
---
 .../13312-attributes+bool_single.rst               | 13 +++++
 doc/sphinx/addendum/type-classes.rst               |  7 ++-
 doc/sphinx/addendum/universe-polymorphism.rst      | 54 +++++++++----------
 doc/sphinx/changes.rst                             |  6 +--
 doc/sphinx/language/core/basic.rst                 |  7 ++-
 doc/sphinx/language/core/coinductive.rst           |  6 +--
 doc/sphinx/language/core/definitions.rst           |  2 +-
 doc/sphinx/language/core/inductive.rst             | 24 ++++-----
 doc/sphinx/language/core/records.rst               |  6 +--
 doc/sphinx/language/core/variants.rst              |  6 +--
 doc/sphinx/language/extensions/canonical.rst       | 31 +++++------
 test-suite/success/Template.v                      |  2 +-
 test-suite/success/attribute_syntax.v              | 18 ++++++-
 vernac/attributes.ml                               | 60 +++++++++++++++++-----
 vernac/attributes.mli                              |  7 ++-
 vernac/g_vernac.mlg                                |  2 +-
 16 files changed, 147 insertions(+), 104 deletions(-)
 create mode 100644 doc/changelog/02-specification-language/13312-attributes+bool_single.rst

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..fa046d968f
--- /dev/null
+++ b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst
@@ -0,0 +1,13 @@
+- **Changed:**
+  Boolean attributes are now specified using key/value pairs, that is
+  to say ``attr={yes,no}``. If the value is missing, the default is
+  ``on``.  Old syntax is still supported, but produces the
+  ``deprecated-attribute-syntax`` warning.
+  Attributes deprecated are ``universes(monomorphic)``,
+  ``universes(notemplate)``, ``universes(noncumulative)``, which are
+  replaced by the corresponding ``universes(polymorphic=no)`` etc...
+  Attributes :attr:`program` and :attr:`canonical` are also affected,
+  with the syntax ``attr(false)`` being deprecated in favor of
+  ``attr=no``.
+  (`#13312 <https://github.com/coq/coq/pull/13312>`_,
+  by Emilio Jesus Gallego Arias).
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} _.
 
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 fd4fe3d47d..04b1f128d3 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -156,12 +156,20 @@ let legacy_bool_attribute ~name ~on ~off : bool option attribute =
      (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 ->
-        (* Will insert deprecation warning *)
+        deprecated_bool_attribute_warning name;
         Some v
       | Some v, None -> Some v
       | Some v1, Some v2 ->
@@ -174,8 +182,16 @@ let deprecated_bool_attribute ~name ~on ~off : bool option attribute =
 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 =
@@ -222,21 +238,37 @@ let () = let open Goptions in
 let program =
   enable_attribute ~key:"program" ~default:(fun () -> !program_mode)
 
-let locality =
-  deprecated_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"]
@@ -287,7 +319,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)
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 60195fe790..03a14a03ff 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -88,7 +88,7 @@ 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. *)
 
-(** Define boolean attribute [name], of the form [name={on,off}]. The
+(** 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
 
@@ -99,9 +99,8 @@ val deprecated_bool_attribute
   -> 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
-   [name(on)] [name(off)] and new attribute syntax, with [on] taken as
-   the key. *)
+   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 d9b664e243..116cfc6413 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -137,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" ->
-- 
cgit v1.2.3


From 0af10d808de19f1f052fab3c757f4049fa0c3ec8 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 14 Nov 2020 02:35:55 +0100
Subject: [attributes] Add overlays for #13312

---
 dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh

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
-- 
cgit v1.2.3


From 3b479357d8c5c1a655b2b8257f14a8cafe7621fc Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sat, 14 Nov 2020 16:01:00 +0100
Subject: Run doc_grammar for #13312.

---
 doc/sphinx/language/core/basic.rst | 1 +
 doc/tools/docgram/fullGrammar      | 1 +
 doc/tools/docgram/orderedGrammar   | 1 +
 3 files changed, 3 insertions(+)

diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index af5c47dba8..ea29da6dd4 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 }
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 "," ")"
 ]
 
-- 
cgit v1.2.3


From ca42305f1ed1699065cffdef7d96bf5fcc0069be Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sat, 14 Nov 2020 18:44:57 +0100
Subject: Review commit: improving the doc of boolean attributes.

---
 .../13312-attributes+bool_single.rst               | 22 ++++++----
 doc/sphinx/addendum/program.rst                    |  8 ++--
 doc/sphinx/addendum/universe-polymorphism.rst      | 49 ++++++++++++++--------
 doc/sphinx/language/core/basic.rst                 | 26 ++++++------
 doc/sphinx/language/core/inductive.rst             | 15 +++++--
 doc/sphinx/language/extensions/canonical.rst       |  7 +++-
 6 files changed, 76 insertions(+), 51 deletions(-)

diff --git a/doc/changelog/02-specification-language/13312-attributes+bool_single.rst b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst
index fa046d968f..f069bc616b 100644
--- a/doc/changelog/02-specification-language/13312-attributes+bool_single.rst
+++ b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst
@@ -1,13 +1,17 @@
 - **Changed:**
-  Boolean attributes are now specified using key/value pairs, that is
-  to say ``attr={yes,no}``. If the value is missing, the default is
-  ``on``.  Old syntax is still supported, but produces the
-  ``deprecated-attribute-syntax`` warning.
-  Attributes deprecated are ``universes(monomorphic)``,
-  ``universes(notemplate)``, ``universes(noncumulative)``, which are
-  replaced by the corresponding ``universes(polymorphic=no)`` etc...
+  :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 ``attr(false)`` being deprecated in favor of
-  ``attr=no``.
+  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/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index a2ed23335e..3790f36e5a 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -122,25 +122,32 @@ 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 boolean attribute can be used to control whether universe
+   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 ``polymorphic=no`` is set, global universe constraints
+   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`).
 
+.. attr:: universes(monomorphic)
+
+   .. deprecated:: 8.13
+
+      Use :attr:`universes(polymorphic=no) <universes(polymorphic)>`
+      instead.
+
 .. flag:: Universe Polymorphism
 
    This flag is off by default.  When it is on, new declarations are
-   polymorphic unless the :attr:`universes(polymorphic)` attribute is
-   used to override the default.
+   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
@@ -168,18 +175,23 @@ attribute is used:
 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.
 
+   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.
 
@@ -192,20 +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 } }) ]`.
 
-   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`).
+.. attr:: universes(noncumulative)
+
+   .. deprecated:: 8.13
+
+      Use :attr:`universes(cumulative=no) <universes(cumulative)>` instead.
 
 .. 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(cumulative)` attribute with setting ``off`` is
-   used.  It has no effect on *monomorphic* inductive definitions.
+   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/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index ea29da6dd4..2b262b89c0 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -380,24 +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.
 
-Boolean attributes take the form ``attr={yes,no}``, when the key is
-omitted the default is assumed to be ``yes``.
+: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(polymorphic)`
-`Cumulative`      :attr:`universes(cumulative)`
-`NonCumulative`   :attr:`universes(cumulative)`
-`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/inductive.rst b/doc/sphinx/language/core/inductive.rst
index b9453650eb..251b5e4955 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -1056,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(template)`
-   attribute with the ``=no`` setting.
+   This can be prevented using the :attr:`universes(template=no) <universes(template)>`
+   attribute.
 
    Template polymorphism and full universe polymorphism (see Chapter
    :ref:`polymorphicuniverses`) are incompatible, so if the latter is
@@ -1075,9 +1075,10 @@ 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 boolean attribute can be used to explicitly declare an
+   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.
 
@@ -1096,6 +1097,12 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
    inductive type to be template polymorphic, even if the :flag:`Auto
    Template Polymorphism` flag is on.
 
+.. attr:: universes(notemplate)
+
+   .. 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
 whose sort is in the Type hierarchy. Then, the polymorphism is over
diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst
index ec3e3e8aa6..f7ce7f1c6c 100644
--- a/doc/sphinx/language/extensions/canonical.rst
+++ b/doc/sphinx/language/extensions/canonical.rst
@@ -87,7 +87,8 @@ 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
+.. attr:: canonical{? = {| yes | no } }
+   :name: canonical
 
    This boolean attribute can decorate a :cmd:`Definition` or
    :cmd:`Let` command.  It is equivalent to having a :cmd:`Canonical
@@ -106,7 +107,7 @@ in :ref:`canonicalstructures`; here only a simple example is given.
 
          #[canonical=no] Prf_equiv : equivalence Carrier Equal
 
-   See :ref:`canonicalstructures` for a more realistic example.
+   See :ref:`hierarchy_of_structures` for a more realistic example.
 
 .. cmd:: Print Canonical Projections {* @reference }
 
@@ -245,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
 ----------------------------
 
-- 
cgit v1.2.3


From 6aeee2e4e37d4b8ffb8c50c109903ad336c8bdfa Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 15 Nov 2020 15:57:37 +0100
Subject: [attributes] Update error message referring to deprecated syntax.

---
 doc/sphinx/addendum/universe-polymorphism.rst | 2 +-
 vernac/vernacentries.ml                       | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 3790f36e5a..4615a8dfca 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -195,7 +195,7 @@ Cumulative, NonCumulative
    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.
+   .. 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
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 2edd9d4d11..0f63dfe5ce 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -674,7 +674,7 @@ 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
-- 
cgit v1.2.3


From efa6673158f5eaa3fc11c0b3d1e3285c4acc129a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 16 Nov 2020 16:18:06 +0100
Subject: [attributes] Add output test suite for errors, improve error
 printing.

---
 test-suite/output/attributes.out | 11 +++++++++++
 test-suite/output/attributes.v   |  9 +++++++++
 vernac/attributes.ml             |  9 +++++++--
 3 files changed, 27 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/output/attributes.out
 create mode 100644 test-suite/output/attributes.v

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/vernac/attributes.ml b/vernac/attributes.ml
index 04b1f128d3..fdaeedef8c 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -121,6 +121,9 @@ let single_key_parser ~name ~key v prev args =
   assert_once ~name prev;
   v
 
+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)] *)
@@ -135,13 +138,15 @@ let key_value_attribute ~key ~default ~(values : (string * 'a) list) : 'a option
             | exception Not_found ->
               CErrors.user_err
                 Pp.(str "Invalid value '" ++ str b ++ str "' for key " ++ str key ++ fnl () ++
-                    str "use one of " ++ (pr_sequence str (List.map fst values)))
+                    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 "=value instead.")
+          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]
-- 
cgit v1.2.3