Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.

Ack-by: SkySkimmer
Reviewed-by: jfehrle
Reviewed-by: ppedrot

16 files changed, 362 insertions, 353 deletions

diff --git a/doc/changelog/07-commands-and-options/11162-local-cs.rst b/doc/changelog/07-commands-and-options/11162-local-cs.rst
index 638222fbe1..b89e047153 100644
--- a/doc/changelog/07-commands-and-options/11162-local-cs.rst
+++ b/doc/changelog/07-commands-and-options/11162-local-cs.rst
@@ -1,3 +1,3 @@
-- **Added:** Handle the ``#[local]`` attribute in :g:`Canonical
+- **Added:** Handle the :attr:`local` attribute in :cmd:`Canonical
   Structure` declarations (`#11162
   <https://github.com/coq/coq/pull/11162>`_, by Enrico Tassi).
diff --git a/doc/changelog/07-commands-and-options/11546-rm-uncheck-template.rst b/doc/changelog/07-commands-and-options/11546-rm-uncheck-template.rst
new file mode 100644
index 0000000000..d134aeae8b
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11546-rm-uncheck-template.rst
@@ -0,0 +1,5 @@
+- **Removed:** Deprecated unsound compatibility ``Template Check``
+  flag that was introduced in 8.10 to help users gradually move their
+  template polymorphic inductive type definitions outside sections
+  (`#11546 <https://github.com/coq/coq/pull/11546>`_, by Pierre-Marie
+  Pédrot).
diff --git a/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst b/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst
index 1f8dcd3992..419d683037 100644
--- a/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst
+++ b/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst
@@ -1,5 +1,6 @@
 - **Removed:**
   Unqualified ``polymorphic``, ``monomorphic``, ``template``,
   ``notemplate`` attributes (they were deprecated since Coq 8.10).
-  Use them as sub-attributes of the ``universes`` attribute (`#11663
-  <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann).
+  Use :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`,
+  :attr:`universes(template)` and :attr:`universes(notemplate)` instead
+  (`#11663 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann).
diff --git a/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst b/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst
new file mode 100644
index 0000000000..b6a034941d
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst
@@ -0,0 +1,12 @@
+- **Added:**
+  New attributes supported when defining an inductive type
+  :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and
+  :attr:`private(matching)`, which correspond to legacy attributes
+  ``Cumulative``, ``NonCumulative``, and the so far undocumented
+  ``Private`` (`#11665 <https://github.com/coq/coq/pull/11665>`_, by
+  Théo Zimmermann).
+
+- **Changed:**
+  Legacy attributes can now be passed in any order.  See
+  :ref:`gallina-attributes` (`#11665
+  <https://github.com/coq/coq/pull/11665>`_, by Théo Zimmermann).
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 549249d25c..cbb5c0db8a 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -98,10 +98,17 @@ coercions.
 .. flag:: Program Mode
 
    Enables the program mode, in which 1) typechecking allows subset coercions and
-   2) the elaboration of pattern matching of :cmd:`Program Fixpoint` and
-   :cmd:`Program Definition` act
-   like Program Fixpoint/Definition, generating obligations if there are
-   unresolved holes after typechecking.
+   2) the elaboration of pattern matching of :cmd:`Fixpoint` and
+   :cmd:`Definition` act as if the :attr:`program` attribute had been
+   used, generating obligations if there are unresolved holes after
+   typechecking.
+
+.. attr:: program
+
+   This attribute allows to use the Program mode on a specific
+   definition.  An alternative syntax is to use the legacy ``Program``
+   prefix (cf. :n:`@legacy_attr`) as documented in the rest of this
+   chapter.
 
 .. _syntactic_control:
 
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 7abeca7815..bd4c276571 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -47,7 +47,7 @@ Leibniz equality on some type. An example implementation is:
          | tt, tt => eq_refl tt
          end }.
 
-Using the attribute ``refine``, if the term is not sufficient to
+Using the :attr:`refine` attribute, if the term is not sufficient to
 finish the definition (e.g. due to a missing field or non-inferable
 hole) it must be finished in proof mode. If it is sufficient a trivial
 proof mode with no open goals is started.
@@ -77,9 +77,9 @@ remaining fields, e.g.:
    Defined.
 
 One has to take care that the transparency of every field is
-determined by the transparency of the :cmd:`Instance` proof. One can use
-alternatively the :cmd:`Program Instance` variant which has richer facilities
-for dealing with obligations.
+determined by the transparency of the :cmd:`Instance` proof. One can
+use alternatively the :attr:`program` attribute to get richer
+facilities for dealing with obligations.
 
 
 Binding classes
@@ -174,7 +174,7 @@ For example:
 
 .. coqtop:: in
 
-   Global Program Instance option_eqb : EqDec (option A) :=
+   #[ global, program ] Instance option_eqb : EqDec (option A) :=
      { eqb x y := match x, y with
             | Some x, Some y => eqb x y
             | None, None => true
@@ -188,7 +188,7 @@ For example:
 
    About option_eqb.
 
-Here the :cmd:`Global` modifier redeclares the instance at the end of the
+Here the :attr:`global` attribute redeclares the instance at the end of the
 section, once it has been generalized by the context variables it
 uses.
 
@@ -300,9 +300,11 @@ Summary of the commands
    The :cmd:`Class` command is used to declare a typeclass with parameters
    :token:`binders` and fields the declared record fields.
 
-   This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`,
+   Like any command declaring a record, this command supports the
+   :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`,
    :attr:`universes(template)`, :attr:`universes(notemplate)`,
-   :attr:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes.
+   :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and
+   :attr:`private(matching)` attributes.
 
    .. _singleton-class:
 
@@ -341,6 +343,25 @@ Summary of the commands
    :tacn:`auto` hints. If the priority :token:`num` is not specified, it defaults to the number
    of non-dependent binders of the instance.
 
+   This command supports the :attr:`global` attribute that can be
+   used on instances declared in a section so that their
+   generalization is automatically redeclared after the section is
+   closed.
+
+   Like :cmd:`Definition`, it also supports the :attr:`program`
+   attribute to switch the type checking to `Program` (chapter
+   :ref:`programs`) and use the obligation mechanism to manage missing
+   fields.
+
+   Finally, it supports the lighter :attr:`refine` attribute:
+
+   .. attr:: refine
+
+      This attribute can be used to leave holes or not provide all
+      fields in the definition of an instance and open the tactic mode
+      to fill them.  It works exactly as if no body had been given and
+      the :tacn:`refine` tactic has been used first.
+
    .. cmdv:: Instance @ident {* @binder } : forall {* @binder }, @term__0 {+ @term} {? | @num } := @term
 
       This syntax is used for declaration of singleton class instances or
@@ -348,19 +369,6 @@ Summary of the commands
       {+ @term}`.  One need not even mention the unique field name for
       singleton classes.
 
-   .. cmdv:: Global Instance
-      :name: Global Instance
-
-      One can use the :cmd:`Global` modifier on instances declared in a
-      section so that their generalization is automatically redeclared
-      after the section is closed.
-
-   .. cmdv:: Program Instance
-      :name: Program Instance
-
-      Switches the type checking to `Program` (chapter :ref:`programs`) and
-      uses the obligation mechanism to manage missing fields.
-
    .. cmdv:: Declare Instance
       :name: Declare Instance
 
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 0e326f45d2..a08495badd 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -122,62 +122,92 @@ in a universe strictly higher than :g:`Set`.
 Polymorphic, Monomorphic
 -------------------------
 
-.. cmd:: Polymorphic @definition
+.. attr:: universes(polymorphic)
 
-   As shown in the examples, polymorphic definitions and inductives can be
-   declared using the ``Polymorphic`` prefix.
+   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.
 
 .. flag:: Universe Polymorphism
 
-   Once enabled, this flag will implicitly prepend ``Polymorphic`` to any
-   definition of the user.
+   This flag is off by default.  When it is on, new declarations are
+   polymorphic unless the :attr:`universes(monomorphic)` attribute is
+   used.
 
-.. cmd:: Monomorphic @definition
+.. attr:: universes(monomorphic)
 
-   When the :flag:`Universe Polymorphism` flag is set, to make a definition
-   producing global universe constraints, one can use the ``Monomorphic`` prefix.
+   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`).
 
-Many other commands support the ``Polymorphic`` flag, including:
+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:
 
-.. TODO add links on each of these?
+- :cmd:`Lemma`, :cmd:`Axiom`, etc. can be used to declare universe
+  polymorphic constants.
 
-- ``Lemma``, ``Axiom``, and all the other “definition” keywords support
-  polymorphism.
+- Using the :attr:`universes(polymorphic)` attribute with the
+  :cmd:`Section` command will locally set the polymorphism flag inside
+  the section.
 
-- :cmd:`Section` will locally set the polymorphism flag inside the section.
+- :cmd:`Variable`, :cmd:`Context`, :cmd:`Universe` and
+  :cmd:`Constraint` in a section support polymorphism. See
+  :ref:`universe-polymorphism-in-sections` for more details.
 
-- ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support
-  polymorphism. See :ref:`universe-polymorphism-in-sections` for more details.
-
-- :cmd:`Hint Resolve` and :cmd:`Hint Rewrite` will use the auto/rewrite hint
-  polymorphically, not at a single instance.
+- Using the :attr:`universes(polymorphic)` attribute with the
+  :cmd:`Hint Resolve` or :cmd:`Hint Rewrite` commands will make
+  :tacn:`auto` / :tacn:`rewrite` use the hint polymorphically, not at
+  a single instance.
 
 .. _cumulative:
 
 Cumulative, NonCumulative
 -------------------------
 
-Polymorphic inductive types, coinductive types, variants and records can be
-declared cumulative using the :g:`Cumulative` prefix.
+.. attr:: universes(cumulative)
+
+   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
+   shown in the examples, is more commonly used.
 
-.. cmd:: Cumulative @inductive
+   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.
 
-   Declares the inductive as cumulative
+   .. exn:: The cumulative and noncumulative attributes can only be used in a polymorphic context.
 
-Alternatively, there is a :flag:`Polymorphic Inductive
-Cumulativity` flag which when set, makes all subsequent *polymorphic*
-inductive definitions cumulative.  When set, inductive types and the
-like can be enforced to be non-cumulative using the :g:`NonCumulative`
-prefix.
+      Using this attribute requires being in a polymorphic context,
+      i.e. either having the :flag:`Universe Polymorphism` flag on, or
+      having used the :attr:`universes(polymorphic)` attribute as
+      well.
 
-.. cmd:: NonCumulative @inductive
+   .. note::
 
-   Declares the inductive as non-cumulative
+      ``#[ universes(polymorphic), universes(cumulative) ]`` can be
+      abbreviated into ``#[ universes(polymorphic, cumulative) ]``.
 
 .. flag:: Polymorphic Inductive Cumulativity
 
-   When this flag is on, it sets all following polymorphic inductive
-   types as cumulative (it is off by default).
+   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)
+
+   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.
 
 Consider the examples below.
 
@@ -220,34 +250,10 @@ The following is an example of a record with non-trivial subtyping relation:
    E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη}
    \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j
 
-Cumulative inductive types, coinductive types, variants and records
-only make sense when they are universe polymorphic. Therefore, an
-error is issued whenever the user uses the :g:`Cumulative` or
-:g:`NonCumulative` prefix in a monomorphic context.
-Notice that this is not the case for the :flag:`Polymorphic Inductive Cumulativity` flag.
-That is, this flag, when set, makes all subsequent *polymorphic*
-inductive declarations cumulative (unless, of course the :g:`NonCumulative` prefix is used)
-but has no effect on *monomorphic* inductive declarations.
-
-Consider the following examples.
-
-.. coqtop:: all reset
-
-   Fail Monomorphic Cumulative Inductive Unit := unit.
-
-.. coqtop:: all reset
-
-   Fail Monomorphic NonCumulative Inductive Unit := unit.
-
-.. coqtop:: all reset
-
-   Set Polymorphic Inductive Cumulativity.
-   Inductive Unit := unit.
-
 An example of a proof using cumulativity
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. coqtop:: in
+.. coqtop:: in reset
 
    Set Universe Polymorphism.
    Set Polymorphic Inductive Cumulativity.
@@ -368,10 +374,14 @@ to universes and explicitly instantiate polymorphic definitions.
    In the monorphic case, this command declares a new global universe
    named :g:`ident`, which can be referred to using its qualified name
    as well. Global universe names live in a separate namespace. The
-   command supports the ``Polymorphic`` flag only in sections, meaning the
-   universe quantification will be discharged on each section definition
+   command supports the :attr:`universes(polymorphic)` attribute (or
+   the ``Polymorphic`` prefix) only in sections, meaning the universe
+   quantification will be discharged on each section definition
    independently.
 
+   .. exn:: Polymorphic universes can only be declared inside sections, use Monomorphic Universe instead.
+      :undocumented:
+
 .. cmd:: Constraint @univ_constraint
          Polymorphic Constraint @univ_constraint
 
@@ -379,9 +389,10 @@ to universes and explicitly instantiate polymorphic definitions.
 
    If consistent, the constraint is then enforced in the global
    environment. Like :cmd:`Universe`, it can be used with the
-   ``Polymorphic`` prefix in sections only to declare constraints
-   discharged at section closing time. One cannot declare a global
-   constraint on polymorphic universes.
+   :attr:`universes(polymorphic)` attribute (or the ``Polymorphic``
+   prefix) in sections only to declare constraints discharged at
+   section closing time. One cannot declare a global constraint on
+   polymorphic universes.
 
    .. exn:: Undeclared universe @ident.
       :undocumented:
@@ -389,6 +400,9 @@ to universes and explicitly instantiate polymorphic definitions.
    .. exn:: Universe inconsistency.
       :undocumented:
 
+   .. exn:: Polymorphic universe constraints can only be declared inside sections, use Monomorphic Constraint instead
+      :undocumented:
+
 
 Polymorphic definitions
 ~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index afe22d24e5..a0cf9730a9 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -222,7 +222,7 @@ Changes in 8.11+beta1
 
   .. _811RefineInstance:
 
-- **Added:** ``#[refine]`` attribute for :cmd:`Instance`, a more
+- **Added:** :attr:`refine` attribute for :cmd:`Instance`, a more
   predictable version of the old ``Refine Instance Mode`` which
   unconditionally opens a proof (`#10996
   <https://github.com/coq/coq/pull/10996>`_, by Gaëtan Gilbert).
@@ -1316,7 +1316,7 @@ Changes in 8.10+beta3
   rules governing template-polymorphic types.
 
   To help users incrementally fix this issue, a command line option
-  `-no-template-check` and a global flag :flag:`Template Check` are
+  `-no-template-check` and a global flag ``Template Check`` are
   available to selectively disable the new check. Use at your own risk.
 
   (`#9918 <https://github.com/coq/coq/pull/9918>`_, by Matthieu Sozeau
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 3d77d07061..c2c1c68f5c 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -186,9 +186,7 @@ nitpick_ignore = [ ('token', token) for token in [
     'assums',
     'binders',
     'collection',
-    'definition',
     'dirpath',
-    'inductive',
     'ind_body',
     'modpath',
     'module',
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 4beaff70f5..b0acd09af6 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1200,45 +1200,47 @@ 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 ``universes(notemplate)``
+   This can be prevented using the :attr:`universes(notemplate)`
    attribute.
 
+   Template polymorphism and full universe polymorphism (see Chapter
+   :ref:`polymorphicuniverses`) are incompatible, so if the latter is
+   enabled (through the :flag:`Universe Polymorphism` flag or the
+   :attr:`universes(polymorphic)` attribute) it will prevail over
+   automatic template polymorphism.
+
 .. warn:: Automatically declaring @ident as template polymorphic.
 
-   Warning ``auto-template`` can be used to find which types are
-   implicitly declared template polymorphic by :flag:`Auto Template
-   Polymorphism`.
+   Warning ``auto-template`` can be used (it is off by default) to
+   find which types are implicitly declared template polymorphic by
+   :flag:`Auto Template Polymorphism`.
 
    An inductive type can be forced to be template polymorphic using
-   the ``universes(template)`` attribute: it should then fulfill the
-   criterion to be template polymorphic or an error is raised.
-
-.. exn:: Inductive @ident cannot be made template polymorphic.
-
-   This error is raised when the `#[universes(template)]` attribute is
-   on but the inductive cannot be made polymorphic on any universe or be
-   inferred to live in :math:`\Prop` or :math:`\Set`.
-
-   Template polymorphism and universe polymorphism (see Chapter
-   :ref:`polymorphicuniverses`) are incompatible, so if the later is
-   enabled it will prevail over automatic template polymorphism and
-   cause an error when using the ``universes(template)`` attribute.
-
-.. flag:: Template Check
-
-   This flag is on by default. Turning it off disables the check of
-   locality of the sorts when abstracting the inductive over its
-   parameters. This is a deprecated and *unsafe* flag that can introduce
-   inconsistencies, it is only meant to help users incrementally update
-   code from Coq versions < 8.10 which did not implement this check.
-   The `Coq89.v` compatibility file sets this flag globally. A global
-   ``-no-template-check`` command line option is also available. Use at
-   your own risk. Use of this flag is recorded in the typing flags
-   associated to a definition but is *not* supported by the |Coq|
-   checker (`coqchk`). It will appear in :g:`Print Assumptions` and
-   :g:`About @ident` output involving inductive declarations that were
-   (potentially unsoundly) assumed to be template polymorphic.
+   the :attr:`universes(template)` attribute: in this case, the
+   warning is not emitted.
+
+.. 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.
+
+   .. exn:: template and polymorphism not compatible
+
+      This attribute cannot be used in a full universe polymorphic
+      context, i.e. if the :flag:`Universe Polymorphism` flag is on or
+      if the :attr:`universes(polymorphic)` attribute is used.
+
+   .. exn:: Ill-formed template inductive declaration: not polymorphic on any universe.
+
+      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.
 
 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/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index b9e181dd94..eff5eb60eb 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -42,9 +42,11 @@ 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:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes.
+   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.
 
 More generally, a record may have explicitly defined (a.k.a. manifest)
 fields. For instance, we might have:
@@ -2053,12 +2055,15 @@ applied to an unknown structure instance (an implicit argument) and a
 value. The complete documentation of canonical structures can be found
 in :ref:`canonicalstructures`; here only a simple example is given.
 
-.. cmd:: {? Local | #[local] } Canonical {? Structure } @qualid
+.. cmd:: Canonical {? Structure } @qualid
   :name: Canonical Structure
 
    This command declares :token:`qualid` as a canonical instance of a
-   structure (a record). When the :g:`#[local]` attribute is given the effect
-   stops at the end of the :g:`Section` containig it.
+   structure (a record).
+
+   This command supports the :attr:`local` attribute.  When used, the
+   structure stops being a canonical instance at the end of the
+   :cmd:`Section` containing it.
 
    Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the
    structure :g:`struct` of which the fields are |x_1|, …, |x_n|.
@@ -2106,9 +2111,12 @@ 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.
 
-   .. note::
-      To prevent a field from being involved in the inference of canonical instances,
-      its declaration can be annotated with the :g:`#[canonical(false)]` attribute.
+   .. 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`).
 
       .. example::
 
@@ -2121,11 +2129,17 @@ in :ref:`canonicalstructures`; here only a simple example is given.
 
       See :ref:`canonicalstructures` for a more realistic example.
 
-   .. cmdv:: {? Local | #[local] } Canonical {? Structure } @ident {? : @type } := @term
+   .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term
 
       This is equivalent to a regular definition of :token:`ident` followed by the
       declaration :n:`Canonical @ident`.
 
+.. attr:: canonical
+
+   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.
+
 .. cmd:: Print Canonical Projections {* @ident}
 
    This displays the list of global names that are components of some
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 4f0cf5f815..e710e19c12 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -767,6 +767,10 @@ Section :ref:`typing-rules`.
    If :n:`@reduce` is present then :n:`@ident` is bound to the result of the specified
    computation on :n:`@term`.
 
+   These commands also support the :attr:`universes(polymorphic)`,
+   :attr:`universes(monomorphic)`, :attr:`program` and
+   :attr:`canonical` attributes.
+
    If :n:`@term` is omitted, Coq enters the proof editing mode.  This can be
    used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
    In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
@@ -821,9 +825,11 @@ Inductive types
    may be impossible to derive (for example, when :n:`@ident` is a
    proposition).
 
-   This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`,
-   :attr:`universes(template)`, :attr:`universes(notemplate)`,
-   :attr:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes.
+   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.
 
    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.
@@ -851,9 +857,9 @@ Inductive types
       :n:`@ident` being defined (or :n:`@ident` applied to arguments in
       the case of annotated inductive types — cf. next section).
 
-The following subsections show examples of simple inductive types, simple annotated
-inductive types, simple parametric inductive types and mutually inductive
-types.
+The following subsections show examples of simple inductive types,
+simple annotated inductive types, simple parametric inductive types,
+mutually inductive types and private (matching) inductive types.
 
 .. _simple-inductive-types:
 
@@ -1122,6 +1128,31 @@ Mutually defined inductive types
    A generic command :cmd:`Scheme` is useful to build automatically various
    mutual induction principles.
 
+Private (matching) inductive types
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. attr:: private(matching)
+
+   This attribute can be used to forbid the use of the :g:`match`
+   construct on objects of this inductive type outside of the module
+   where it is defined.  There is also a legacy syntax using the
+   ``Private`` prefix (cf. :n:`@legacy_attr`).
+
+   The main use case of private (matching) inductive types is to emulate
+   quotient types / higher-order inductive types in projects such as
+   the `HoTT library <https://github.com/HoTT/HoTT>`_.
+
+.. example::
+
+   .. coqtop:: all
+
+      Module Foo.
+      #[ private(matching) ] Inductive my_nat := my_O : my_nat | my_S : my_nat -> my_nat.
+      Check (fun x : my_nat => match x with my_O => true | my_S _ => false end).
+      End Foo.
+      Import Foo.
+      Fail Check (fun x : my_nat => match x with my_O => true | my_S _ => false end).
+
 Variants
 ~~~~~~~~
 
@@ -1132,9 +1163,11 @@ Variants
    be defined using :cmd:`Variant`). No induction scheme is generated for
    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:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes.
+   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.
 
    .. exn:: The @num th argument of @ident must be @ident in @type.
       :undocumented:
@@ -1160,9 +1193,11 @@ of the type.
    type, since such principles only make sense for inductive types.
    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:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes.
+   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.
 
 .. example::
 
@@ -1607,14 +1642,21 @@ the proof and adds it to the environment.
 Attributes
 -----------
 
-.. insertprodn all_attrs legacy_attrs
+.. insertprodn all_attrs legacy_attr
 
 .. prodn::
-   all_attrs ::= {* #[ {*, @attr } ] } {? @legacy_attrs }
+   all_attrs ::= {* #[ {*, @attr } ] } {* @legacy_attr }
    attr ::= @ident {? @attr_value }
    attr_value ::= = @string
    | ( {*, @attr } )
-   legacy_attrs ::= {? {| Local | Global } } {? {| Polymorphic | Monomorphic } } {? Program } {? {| Cumulative | NonCumulative } } {? Private }
+   legacy_attr ::= Local
+   | Global
+   | Polymorphic
+   | Monomorphic
+   | Cumulative
+   | NonCumulative
+   | Private
+   | Program
 
 Attributes modify the behavior of a command or tactic.
 Syntactically, most commands and tactics can be decorated with attributes, but
@@ -1623,7 +1665,7 @@ attributes not supported by the command or tactic will be flagged as errors.
 The order of top-level attributes doesn't affect their meaning.  ``#[foo,bar]``, ``#[bar,foo]``,
 ``#[foo]#[bar]`` and ``#[bar]#[foo]`` are equivalent.
 
-The legacy attributes (:n:`@legacy_attrs`) provide an older, alternate syntax
+The legacy attributes (:n:`@legacy_attr`) provide an older, alternate syntax
 for certain attributes.  They are equivalent to new attributes as follows:
 
 ================  ================================
@@ -1633,65 +1675,12 @@ Legacy attribute  New attribute
 `Global`          :attr:`global`
 `Polymorphic`     :attr:`universes(polymorphic)`
 `Monomorphic`     :attr:`universes(monomorphic)`
-`Cumulative`      none
-`NonCumulative`   none
-`Private`         none
+`Cumulative`      :attr:`universes(cumulative)`
+`NonCumulative`   :attr:`universes(noncumulative)`
+`Private`         :attr:`private(matching)`
 `Program`         :attr:`program`
 ================  ================================
 
-Some attributes are specific to a command, and so are described with
-that command. Currently, the following attributes are recognized:
-
-.. attr:: universes(monomorphic)
-   :name: universes(monomorphic)
-
-   See :ref:`polymorphicuniverses`.
-
-.. attr:: universes(polymorphic)
-   :name: universes(polymorphic)
-
-   See :ref:`polymorphicuniverses`.
-
-.. attr:: universes(template)
-   :name: universes(template)
-
-   See :ref:`Template-polymorphism`
-
-.. attr:: universes(notemplate)
-   :name: universes(notemplate)
-
-   See :ref:`Template-polymorphism`
-
-.. attr:: program
-
-   See :ref:`programs`.
-
-.. attr:: global
-
-   See :ref:`controlling-locality-of-commands`.
-
-.. attr:: local
-
-   See :ref:`controlling-locality-of-commands`.
-
-.. attr:: Cumulative
-
-   Legacy attribute, only allowed in a polymorphic context.
-   Specifies that two instances of the same inductive type (family) are convertible
-   based on the universe variances; they do not need to be equal.
-   See :ref:`cumulative`.
-
-.. attr:: NonCumulative
-
-   Legacy attribute, only allowed in a polymorphic context.
-   Specifies that two instances of the same inductive type (family) are convertible
-   only if all the universes are equal.
-   See :ref:`cumulative`.
-
-.. attr:: Private
-
-   Legacy attribute.  Documentation to be added.
-
 .. attr:: deprecated ( {? since = @string , } {? note = @string } )
    :name: deprecated
 
@@ -1703,46 +1692,24 @@ that command. Currently, the following attributes are recognized:
 
     It can trigger the following warnings:
 
-    .. warn:: Tactic @qualid is deprecated since @string. @string.
-       :undocumented:
-
-    .. warn:: Tactic Notation @qualid is deprecated since @string. @string.
-       :undocumented:
-
-    .. warn:: Notation @string__1 is deprecated since @string__2. @string__3.
-
-       :n:`@string__1` is the actual notation, :n:`@string__2` is the version number,
-       :n:`@string__3` is the note.
-
-.. attr:: canonical
+    .. warn:: Tactic @qualid is deprecated since @string__since. @string__note.
+              Tactic Notation @qualid is deprecated since @string__since. @string__note.
+              Notation @string is deprecated since @string__since. @string__note.
 
-    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.
-
-    This attribute can take the value ``false`` when decorating a record field
-    declaration with the effect of preventing the field from being involved in
-    the inference of canonical instances.
-
-    See also :ref:`canonical-structure-declaration`.
-
-.. example::
+       :n:`@qualid` or :n:`@string` is the notation, :n:`@string__since` is the version number,
+       :n:`@string__note` is the note (usually explains the replacement).
 
-   .. coqtop:: all reset warn
+    .. example::
 
-        From Coq Require Program.
-        #[program] Definition one : nat := S _.
-        Next Obligation.
-          exact O.
-        Defined.
+       .. coqtop:: all reset warn
 
-        #[deprecated(since="8.9.0", note="Use idtac instead.")]
-        Ltac foo := idtac.
+          #[deprecated(since="8.9.0", note="Use idtac instead.")]
+          Ltac foo := idtac.
 
-        Goal True.
-        Proof.
+          Goal True.
+          Proof.
           now foo.
-        Abort.
+          Abort.
 
 .. warn:: Unsupported attribute
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 4401f8fa2f..895886605d 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -91,34 +91,30 @@ and tables:
 Flags, options and tables are identified by a series of identifiers, each with an initial
 capital letter.
 
-.. cmd::  {? {| Local | Global | Export } } Set @flag
+.. cmd::  Set @flag
    :name: Set
 
-   Sets :token:`flag` on. Scoping qualifiers are
-   described :ref:`here <set_unset_scope_qualifiers>`.
+   Sets :token:`flag` on.
 
-.. cmd:: {? {| Local | Global | Export } } Unset @flag
+.. cmd:: Unset @flag
    :name: Unset
 
-   Sets :token:`flag` off. Scoping qualifiers are
-   described :ref:`here <set_unset_scope_qualifiers>`.
+   Sets :token:`flag` off.
 
 .. cmd:: Test @flag
 
    Prints the current value of :token:`flag`.
 
 
-.. cmd:: {? {| Local | Global | Export } } Set @option {| @num | @string }
+.. cmd:: Set @option {| @num | @string }
    :name: Set @option
 
-   Sets :token:`option` to the specified value.  Scoping qualifiers are
-   described :ref:`here <set_unset_scope_qualifiers>`.
+   Sets :token:`option` to the specified value.
 
-.. cmd:: {? {| Local | Global | Export } } Unset @option
+.. cmd:: Unset @option
    :name: Unset @option
 
-   Sets :token:`option` to its default value.  Scoping qualifiers are
-   described :ref:`here <set_unset_scope_qualifiers>`.
+   Sets :token:`option` to its default value.
 
 .. cmd:: Test @option
 
@@ -157,27 +153,37 @@ capital letter.
 
    A synonym for :cmd:`Print Options`.
 
-.. _set_unset_scope_qualifiers:
+Locality attributes supported by :cmd:`Set` and :cmd:`Unset`
+````````````````````````````````````````````````````````````
+
+The :cmd:`Set` and :cmd:`Unset` commands support the :attr:`local`,
+:attr:`global` and :attr:`export` locality attributes:
+
+* no attribute: the original setting is *not* restored at the end of
+  the current module or section.
+* :attr:`local` (an alternative syntax is to use the ``Local``
+  prefix): the setting is applied within the current module or
+  section.  The original value of the setting is restored at the end
+  of the current module or section.
+* :attr:`export` (an alternative syntax is to use the ``Export``
+  prefix): similar to :attr:`local`, the original value of the setting
+  is restored at the end of the current module or section.  In
+  addition, if the value is set in a module, then :cmd:`Import`\-ing
+  the module sets the option or flag.
+* :attr:`global` (an alternative syntax is to use the ``Global``
+  prefix): the original setting is *not* restored at the end of the
+  current module or section.  In addition, if the value is set in a
+  file, then :cmd:`Require`\-ing the file sets the option.
+
+Newly opened modules and sections inherit the current settings.
 
-Scope qualifiers for :cmd:`Set` and :cmd:`Unset`
-`````````````````````````````````````````````````
-
-:n:`{? {| Local | Global | Export } }`
-
-Flag and option settings can be global in scope or local to nested scopes created by
-:cmd:`Module` and :cmd:`Section` commands.  There are four alternatives:
-
-* no qualifier: the original setting is *not* restored at the end of the current module or section.
-* **Local**: the setting is applied within the current scope.  The original value of the option
-  or flag is restored at the end of the current module or section.
-* **Global**: similar to no qualifier, the original setting is *not* restored at the end of the current
-  module or section.  In addition, if the value is set in a file, then :cmd:`Require`-ing
-  the file sets the option.
-* **Export**: similar to **Local**, the original value of the option or flag is restored at the
-  end of the current module or section.  In addition, if the value is set in a file, then :cmd:`Import`-ing
-  the file sets the option.
+.. note::
 
-Newly opened scopes inherit the current settings.
+   The use of the :attr:`global` attribute with the :cmd:`Set` and
+   :cmd:`Unset` commands is discouraged.  If your goal is to define
+   project-wide settings, you should rather use the command-line
+   arguments ``-set`` and ``-unset`` for setting flags and options
+   (cf. :ref:`command-line-options`).
 
 .. _requests-to-the-environment:
 
@@ -1152,49 +1158,51 @@ described first.
 Controlling the locality of commands
 -----------------------------------------
 
+.. attr:: global
+          local
 
-.. cmd:: Local @command
-         Global @command
-
-   Some commands support a Local or Global prefix modifier to control the
-   scope of their effect. There are four kinds of commands:
-
+   Some commands support a :attr:`local` or :attr:`global` attribute
+   to control the scope of their effect.  There is also a legacy (and
+   much more commonly used) syntax using the ``Local`` or ``Global``
+   prefixes (see :n:`@legacy_attr`).  There are four kinds of
+   commands:
 
    + Commands whose default is to extend their effect both outside the
      section and the module or library file they occur in.  For these
-     commands, the Local modifier limits the effect of the command to the
+     commands, the :attr:`local` attribute limits the effect of the command to the
      current section or module it occurs in.  As an example, the :cmd:`Coercion`
      and :cmd:`Strategy` commands belong to this category.
    + Commands whose default behavior is to stop their effect at the end
      of the section they occur in but to extend their effect outside the module or
-     library file they occur in. For these commands, the Local modifier limits the
+     library file they occur in. For these commands, the :attr:`local` attribute limits the
      effect of the command to the current module if the command does not occur in a
-     section and the Global modifier extends the effect outside the current
+     section and the :attr:`global` attribute extends the effect outside the current
      sections and current module if the command occurs in a section. As an example,
      the :cmd:`Arguments <Arguments (implicits)>`, :cmd:`Ltac` or :cmd:`Notation` commands belong
      to this category. Notice that a subclass of these commands do not support
-     extension of their scope outside sections at all and the Global modifier is not
+     extension of their scope outside sections at all and the :attr:`global` attribute is not
      applicable to them.
    + Commands whose default behavior is to stop their effect at the end
-     of the section or module they occur in.  For these commands, the ``Global``
-     modifier extends their effect outside the sections and modules they
-     occur in.  The :cmd:`Transparent` and :cmd:`Opaque`
-     (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands
+     of the section or module they occur in.  For these commands, the :attr:`global`
+     attribute extends their effect outside the sections and modules they
+     occur in.  The :cmd:`Transparent` and :cmd:`Opaque` commands
      belong to this category.
    + Commands whose default behavior is to extend their effect outside
      sections but not outside modules when they occur in a section and to
      extend their effect outside the module or library file they occur in
-     when no section contains them. For these commands, the Local modifier
-     limits the effect to the current section or module while the Global
-     modifier extends the effect outside the module even when the command
+     when no section contains them. For these commands, the :attr:`local` attribute
+     limits the effect to the current section or module while the :attr:`global`
+     attribute extends the effect outside the module even when the command
      occurs in a section.  The :cmd:`Set` and :cmd:`Unset` commands belong to this
      category.
 
 .. attr:: export
 
-  Some commands support an :attr:`export` attribute. The effect of the attribute
-  is to make the effect of the command available when the module containing it
-  is imported. The :cmd:`Hint` command accepts it for instance.
+   Some commands support an :attr:`export` attribute.  The effect of
+   the attribute is to make the effect of the command available when
+   the module containing it is imported.  It is supported in
+   particular by the :cmd:`Hint`, :cmd:`Set` and :cmd:`Unset`
+   commands.
 
 .. _controlling-typing-flags:
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index fe2e68a517..5bf122078d 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -140,10 +140,10 @@ field_ident: [
 | "." ident
 ]
 
-basequalid: [
-| REPLACE ident fields
-| WITH ident LIST0 field_ident
-| DELETE ident
+qualid: [ | DELETENT ]
+
+qualid: [
+| ident LIST0 field_ident
 ]
 
 field: [ | DELETENT ]
@@ -387,7 +387,7 @@ gallina: [
 | REPLACE thm_token ident_decl binders ":" lconstr LIST0 [ "with" ident_decl binders ":" lconstr ]
 | WITH thm_token ident_decl binders ":" type LIST0 [ "with" ident_decl binders ":" type ]
 | DELETE assumptions_token inline assum_list
-| REPLACE OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with"
+| REPLACE finite_token LIST1 inductive_definition SEP "with"
 | WITH "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
 |   "CoInductive" inductive_definition LIST0 ( "with" inductive_definition )
 |   "Variant" inductive_definition LIST0 ( "with" inductive_definition )
@@ -405,11 +405,6 @@ gallina: [
 | WITH "Scheme" scheme LIST0 ( "with" scheme )
 ]
 
-DELETE: [
-| private_token
-| cumulativity_token
-]
-
 constructor_list_or_record_decl: [
 | OPTINREF
 ]
@@ -737,12 +732,8 @@ assumption_token: [
 | WITH [ "Variable" | "Variables" ]
 ]
 
-legacy_attrs: [
-| OPT [ "Local" | "Global" ] OPT [ "Polymorphic" | "Monomorphic" ] OPT "Program" OPT [ "Cumulative" | "NonCumulative" ] OPT "Private"
-]
-
 all_attrs: [
-| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) OPT legacy_attrs
+| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) LIST0 legacy_attr
 ]
 
 vernacular: [
@@ -842,7 +833,6 @@ SPLICE: [
 | ne_lstring
 | ne_string
 | lstring
-| basequalid
 | fullyqualid
 | global
 | reference
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 6897437457..2fabf92b7f 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -386,11 +386,6 @@ fullyqualid: [
 | ident
 ]
 
-basequalid: [
-| ident fields
-| ident
-]
-
 name: [
 | "_"
 | ident
@@ -401,6 +396,10 @@ reference: [
 | ident
 ]
 
+qualid: [
+| reference
+]
+
 by_notation: [
 | ne_string OPT [ "%" IDENT ]
 ]
@@ -410,10 +409,6 @@ smart_global: [
 | by_notation
 ]
 
-qualid: [
-| basequalid
-]
-
 ne_string: [
 | STRING
 ]
@@ -436,7 +431,7 @@ lstring: [
 
 integer: [
 | NUMERAL
-| "-" NUMERAL
+| test_minus_nat "-" NUMERAL
 ]
 
 natural: [
@@ -735,21 +730,22 @@ attribute_value: [
 |
 ]
 
-vernac: [
-| "Local" vernac_poly
-| "Global" vernac_poly
-| vernac_poly
+legacy_attr: [
+| "Local"
+| "Global"
+| "Polymorphic"
+| "Monomorphic"
+| "Cumulative"
+| "NonCumulative"
+| "Private"
+| "Program"
 ]
 
-vernac_poly: [
-| "Polymorphic" vernac_aux
-| "Monomorphic" vernac_aux
-| vernac_aux
+vernac: [
+| LIST0 legacy_attr vernac_aux
 ]
 
 vernac_aux: [
-| "Program" gallina "."
-| "Program" gallina_ext "."
 | gallina "."
 | gallina_ext "."
 | command "."
@@ -774,7 +770,7 @@ gallina: [
 | assumptions_token inline assum_list
 | def_token ident_decl def_body
 | "Let" identref def_body
-| OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with"
+| finite_token LIST1 inductive_definition SEP "with"
 | "Fixpoint" LIST1 rec_definition SEP "with"
 | "Let" "Fixpoint" LIST1 rec_definition SEP "with"
 | "CoFixpoint" LIST1 corec_definition SEP "with"
@@ -903,16 +899,6 @@ finite_token: [
 | "Class"
 ]
 
-cumulativity_token: [
-| "Cumulative"
-| "NonCumulative"
-]
-
-private_token: [
-| "Private"
-|
-]
-
 def_body: [
 | binders ":=" reduce lconstr
 | binders ":" lconstr ":=" reduce lconstr
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index f26a174722..c3634466cc 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -172,7 +172,7 @@ vernacular: [
 ]
 
 all_attrs: [
-| LIST0 ( "#[" LIST0 attr SEP "," "]" ) OPT legacy_attrs
+| LIST0 ( "#[" LIST0 attr SEP "," "]" ) LIST0 legacy_attr
 ]
 
 attr: [
@@ -184,8 +184,15 @@ attr_value: [
 | "(" LIST0 attr SEP "," ")"
 ]
 
-legacy_attrs: [
-| OPT [ "Local" | "Global" ] OPT [ "Polymorphic" | "Monomorphic" ] OPT "Program" OPT [ "Cumulative" | "NonCumulative" ] OPT "Private"
+legacy_attr: [
+| "Local"
+| "Global"
+| "Polymorphic"
+| "Monomorphic"
+| "Cumulative"
+| "NonCumulative"
+| "Private"
+| "Program"
 ]
 
 sort: [
@@ -338,20 +345,10 @@ pattern0: [
 ]
 
 vernac: [
-| "Local" vernac_poly
-| "Global" vernac_poly
-| vernac_poly
-]
-
-vernac_poly: [
-| "Polymorphic" vernac_aux
-| "Monomorphic" vernac_aux
-| vernac_aux
+| LIST0 legacy_attr vernac_aux
 ]
 
 vernac_aux: [
-| "Program" gallina "."
-| "Program" gallina_ext "."
 | gallina "."
 | gallina_ext "."
 | command "."