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

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

23 files changed, 473 insertions, 455 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 "."
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index c7dfe69fb1..e08ad9af3a 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1517,7 +1517,7 @@ let do_build_inductive
         in
         let msg =
           str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)})
+            Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(Vernacexpr.Inductive_kw,repacked_rel_inds)})
             ++ fnl () ++
             msg
         in
@@ -1532,7 +1532,7 @@ let do_build_inductive
         in
         let msg =
           str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)})
+            Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(Vernacexpr.Inductive_kw,repacked_rel_inds)})
             ++ fnl () ++
             CErrors.print reraise
         in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 15e839c612..567acb1c73 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -130,7 +130,7 @@ let classify_vernac e =
     | VernacPrimitive (id,_,_) ->
         VtSideff ([id.CAst.v], VtLater)
     | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater)
-    | VernacInductive (_, _,_,l) ->
+    | VernacInductive (_,l) ->
         let ids = List.map (fun (((_,({v=id},_)),_,_,cl),_) -> id :: match cl with
         | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l
         | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @
diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v
index 4717759dec..b403fc120c 100644
--- a/test-suite/success/attribute_syntax.v
+++ b/test-suite/success/attribute_syntax.v
@@ -36,3 +36,10 @@ Check M.zed@{_}.
 Fail Check zed.
 Check M.kats@{_}.
 Fail Check kats.
+
+Export Set Foo.
+
+#[ export ] Set Foo.
+
+Fail #[ export ] Export Foo.
+(* Attribute for Locality specified twice *)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 77423fbadf..dd75693c5b 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -107,35 +107,40 @@ GRAMMAR EXTEND Gram
       | -> { VernacFlagEmpty } ]
     ]
   ;
-  vernac:
-    [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in (("local", VernacFlagEmpty) :: f, v) }
-      | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in (("global", VernacFlagEmpty) :: f, v) }
-
-      | v = vernac_poly -> { v } ]
-    ]
+  legacy_attr:
+    [ [ IDENT "Local" ->
+        { ("local", VernacFlagEmpty) }
+      | IDENT "Global" ->
+        { ("global", VernacFlagEmpty) }
+      | IDENT "Polymorphic" ->
+        { Attributes.vernac_polymorphic_flag }
+      | IDENT "Monomorphic" ->
+        { Attributes.vernac_monomorphic_flag }
+      | IDENT "Cumulative" ->
+        { ("universes", VernacFlagList ["cumulative", VernacFlagEmpty]) }
+      | IDENT "NonCumulative" ->
+        { ("universes", VernacFlagList ["noncumulative", VernacFlagEmpty]) }
+      | IDENT "Private" ->
+        { ("private", VernacFlagList ["matching", VernacFlagEmpty]) }
+      | IDENT "Program" ->
+        { ("program", VernacFlagEmpty) }
+      ] ]
   ;
-  vernac_poly:
-    [ [ IDENT "Polymorphic"; v = vernac_aux ->
-        { let (f, v) = v in (Attributes.vernac_polymorphic_flag :: f, v) }
-      | IDENT "Monomorphic"; v = vernac_aux ->
-        { let (f, v) = v in (Attributes.vernac_monomorphic_flag :: f, v) }
-      | v = vernac_aux -> { v } ]
-    ]
+  vernac:
+    [ [ attrs = LIST0 legacy_attr; v = vernac_aux -> { (attrs, v) } ] ]
   ;
   vernac_aux:
     (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
     (* "." is still in the stream and discard_to_dot works correctly         *)
-    [ [ IDENT "Program"; g = gallina; "." -> { (["program", VernacFlagEmpty], g) }
-      | IDENT "Program"; g = gallina_ext; "." -> { (["program", VernacFlagEmpty], g) }
-      | g = gallina; "." -> { ([], g) }
-      | g = gallina_ext; "." -> { ([], g) }
-      | c = command; "." -> { ([], c) }
-      | c = syntax; "." -> { ([], c) }
-      | c = subprf -> { ([], c) }
+    [ [ g = gallina; "." -> { g }
+      | g = gallina_ext; "." -> { g }
+      | c = command; "." -> { c }
+      | c = syntax; "." -> { c }
+      | c = subprf -> { c }
     ] ]
   ;
   vernac_aux: LAST
-    [ [ prfcom = command_entry -> { ([], prfcom) } ] ]
+    [ [ prfcom = command_entry -> { prfcom } ] ]
   ;
   noedit_mode:
     [ [ c = query_command -> { c None } ] ]
@@ -197,9 +202,8 @@ GRAMMAR EXTEND Gram
       | IDENT "Let"; id = identref; b = def_body ->
           { VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b) }
       (* Gallina inductive declarations *)
-      | cum = OPT cumulativity_token; priv = private_token; f = finite_token;
-        indl = LIST1 inductive_definition SEP "with" ->
-          { VernacInductive (cum, priv, f, indl) }
+      | f = finite_token; indl = LIST1 inductive_definition SEP "with" ->
+          { VernacInductive (f, indl) }
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
           { VernacFixpoint (NoDischarge, recs) }
       | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
@@ -341,13 +345,6 @@ GRAMMAR EXTEND Gram
       | IDENT "Structure" -> { Structure }
       | IDENT "Class" -> { Class true } ] ]
   ;
-  cumulativity_token:
-    [ [ IDENT "Cumulative" -> { VernacCumulative }
-      | IDENT "NonCumulative" -> { VernacNonCumulative } ] ]
-  ;
-  private_token:
-    [ [ IDENT "Private" -> { true } | -> { false } ] ]
-  ;
   (* Simple definitions *)
   def_body:
     [ [ bl = binders; ":="; red = reduce; c = lconstr ->
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 5808c55cfc..a3de88d4dc 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -804,7 +804,7 @@ let string_of_definition_object_kind = let open Decls in function
         let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
         return (hov 2 (pr_assumption_token (n > 1) discharge kind ++
                        pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions))
-      | VernacInductive (cum, p,f,l) ->
+      | VernacInductive (f,l) ->
         let pr_constructor (coe,(id,c)) =
           hov 2 (pr_lident id ++ str" " ++
                    (if coe then str":>" else str":") ++
@@ -830,24 +830,14 @@ let string_of_definition_object_kind = let open Decls in function
               str" :=") ++ pr_constructor_list lc ++
             prlist (pr_decl_notation @@ pr_constr env sigma) ntn
         in
-        let key =
-          let kind =
-            match f with Record -> "Record" | Structure -> "Structure"
-                       | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
-                       | Class _ -> "Class" | Variant -> "Variant"
-          in
-          if p then
-            let cm =
-              match cum with
-              | Some VernacCumulative -> "Cumulative"
-              | Some VernacNonCumulative -> "NonCumulative"
-              | None -> ""
-            in
-            cm ^ " " ^ kind
-          else kind
+        let kind =
+          match f with
+          | Record -> "Record" | Structure -> "Structure"
+          | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
+          | Class _ -> "Class" | Variant -> "Variant"
         in
         return (
-          hov 1 (pr_oneind key (List.hd l)) ++
+          hov 1 (pr_oneind kind (List.hd l)) ++
           (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
         )
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index b5ecd62dad..295db70bc9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -604,17 +604,39 @@ let vernac_assumption ~atts discharge kind l nl =
 
 let is_polymorphic_inductive_cumulativity =
   declare_bool_option_and_ref ~depr:false ~value:false
-    ~key:["Polymorphic"; "Inductive"; "Cumulativity"]
-
-let should_treat_as_cumulative cum poly =
-  match cum with
-  | Some VernacCumulative ->
-    if poly then true
-    else user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.")
-  | Some VernacNonCumulative ->
-    if poly then false
-    else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
-  | None -> poly && is_polymorphic_inductive_cumulativity ()
+    ~key:["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.");
+  in
+  let open Attributes in
+  let open Notations in
+  qualify_attribute "universes"
+    (bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic"
+     ++ bool_attribute ~name:"Cumulativity" ~on:"cumulative" ~off:"noncumulative")
+  >>= function
+  | Some poly, Some cum ->
+     (* Case of Polymorphic|Monomorphic Cumulative|NonCumulative Inductive
+        and #[ universes(polymorphic|monomorphic,cumulative|noncumulative) ] Inductive *)
+     if poly then return (true, cum)
+     else error_poly_context ()
+  | Some poly, None ->
+     (* Case of Polymorphic|Monomorphic Inductive
+        and #[ universes(polymorphic|monomorphic) ] Inductive *)
+     if poly then return (true, is_polymorphic_inductive_cumulativity ())
+     else return (false, false)
+  | None, Some cum ->
+     (* Case of Cumulative|NonCumulative Inductive *)
+     if is_universe_polymorphism () then return (true, cum)
+     else error_poly_context ()
+  | None, None ->
+     (* Case of Inductive *)
+     if is_universe_polymorphism () then
+       return (true, is_polymorphic_inductive_cumulativity ())
+     else
+       return (false, false)
 
 let get_uniform_inductive_parameters =
   Goptions.declare_bool_option_and_ref
@@ -627,8 +649,7 @@ let should_treat_as_uniform () =
   then ComInductive.UniformParameters
   else ComInductive.NonUniformParameters
 
-let vernac_record ~template udecl cum k poly finite records =
-  let cumulative = should_treat_as_cumulative cum poly in
+let vernac_record ~template udecl ~cumulative k ~poly finite records =
   let map ((coe, id), binders, sort, nameopt, cfs) =
     let const = match nameopt with
     | None -> Nameops.add_prefix "Build_" id.v
@@ -668,12 +689,21 @@ let finite_of_kind = let open Declarations in function
   | CoInductive -> CoFinite
   | Variant | Record | Structure | Class _ -> BiFinite
 
-(** When [poly] is true the type is declared polymorphic. When [lo] is true,
-    then the type is declared private (as per the [Private] keyword). [finite]
-    indicates whether the type is inductive, co-inductive or
-    neither. *)
-let vernac_inductive ~atts cum lo kind indl =
-  let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in
+let private_ind =
+  let open Attributes in
+  let open Notations in
+  attribute_of_list
+    [ "matching"
+    , single_key_parser ~name:"Private (matching) inductive type" ~key:"matching" ()
+    ]
+  |> qualify_attribute "private"
+  >>= function
+  | Some () -> return true
+  | None -> return false
+
+let vernac_inductive ~atts kind indl =
+  let (template, (poly, cumulative)), private_ind = Attributes.(
+      parse Notations.(template ++ polymorphic_cumulative ++ private_ind) atts) in
   let open Pp in
   let udecl, indl = extract_inductive_udecl indl in
   if Dumpglob.dump () then
@@ -710,7 +740,7 @@ let vernac_inductive ~atts cum lo kind indl =
     let coe' = if coe then Some true else None in
     let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce),
             { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in
-    vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]]
+    vernac_record ~template udecl ~cumulative (Class true) ~poly finite [id, bl, c, None, [f]]
   else if List.for_all is_record indl then
     (* Mutual record case *)
     let () = match kind with
@@ -735,7 +765,7 @@ let vernac_inductive ~atts cum lo kind indl =
     in
     let kind = match kind with Class _ -> Class false | _ -> kind in
     let recordl = List.map unpack indl in
-    vernac_record ~template udecl cum kind poly finite recordl
+    vernac_record ~template udecl ~cumulative kind ~poly finite recordl
   else if List.for_all is_constructor indl then
     (* Mutual inductive case *)
     let () = match kind with
@@ -758,9 +788,8 @@ let vernac_inductive ~atts cum lo kind indl =
     | RecordDecl _ -> assert false (* ruled out above *)
     in
     let indl = List.map unpack indl in
-    let cumulative = should_treat_as_cumulative cum poly in
     let uniform = should_treat_as_uniform () in
-    ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind:lo ~uniform finite
+    ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uniform finite
   else
     user_err (str "Mixed record-inductive definitions are not allowed")
 
@@ -1464,40 +1493,29 @@ let vernac_set_opacity ~local (v,l) =
   let l = List.map glob_ref l in
   Redexpr.set_strategy local [v,l]
 
-let get_option_locality export local =
-  if export then
-    if Option.is_empty local then OptExport
-    else user_err Pp.(str "Locality modifiers forbidden with Export")
-  else match local with
-  | Some true -> OptLocal
-  | Some false -> OptGlobal
-  | None -> OptDefault
-
-let vernac_set_option0 ~local export key opt =
-  let locality = get_option_locality export local in
+let vernac_set_option0 ~locality key opt =
   match opt with
   | OptionUnset -> unset_option_value_gen ~locality key
   | OptionSetString s -> set_string_option_value_gen ~locality key s
   | OptionSetInt n -> set_int_option_value_gen ~locality key (Some n)
   | OptionSetTrue -> set_bool_option_value_gen ~locality key true
 
-let vernac_set_append_option ~local export key s =
-  let locality = get_option_locality export local in
+let vernac_set_append_option ~locality key s =
   set_string_option_append_value_gen ~locality key s
 
-let vernac_set_option ~local export table v = match v with
+let vernac_set_option ~locality table v = match v with
 | OptionSetString s ->
   (* We make a special case for warnings because appending is their
   natural semantics *)
   if CString.List.equal table ["Warnings"] then
-    vernac_set_append_option ~local export table s
+    vernac_set_append_option ~locality table s
   else
     let (last, prefix) = List.sep_last table in
     if String.equal last "Append" && not (List.is_empty prefix) then
-      vernac_set_append_option ~local export prefix s
+      vernac_set_append_option ~locality prefix s
     else
-      vernac_set_option0 ~local export table v
-| _ -> vernac_set_option0 ~local export table v
+      vernac_set_option0 ~locality table v
+| _ -> vernac_set_option0 ~locality table v
 
 let vernac_add_option key lv =
   let f = function
@@ -2008,8 +2026,8 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
         vernac_declare_module_type lid bl mtys mtyo)
   | VernacAssumption ((discharge,kind),nl,l) ->
     VtDefault(fun () -> with_def_attributes ~atts vernac_assumption discharge kind l nl)
-  | VernacInductive (cum, priv, finite, l) ->
-    VtDefault(fun () -> vernac_inductive ~atts cum priv finite l)
+  | VernacInductive (finite, l) ->
+    VtDefault(fun () -> vernac_inductive ~atts finite l)
   | VernacFixpoint (discharge, l) ->
     let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in
     if opens then
@@ -2164,9 +2182,10 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
     VtDefault(fun () -> with_locality ~atts vernac_set_opacity qidl)
   | VernacSetStrategy l ->
     VtDefault(fun () -> with_locality ~atts vernac_set_strategy l)
-  | VernacSetOption (export, key,v) ->
+  | VernacSetOption (export,key,v) ->
+    let atts = if export then ("export", VernacFlagEmpty) :: atts else atts in
     VtDefault(fun () ->
-        vernac_set_option ~local:(only_locality atts) export key v)
+        vernac_set_option ~locality:(parse option_locality atts) key v)
   | VernacRemoveOption (key,v) ->
     VtDefault(fun () ->
         unsupported_attributes atts;
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index efae1b8dfd..b7c6d3c490 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -250,10 +250,6 @@ type register_kind =
 type module_ast_inl = module_ast * Declaremods.inline
 type module_binder = bool option * lident list * module_ast_inl
 
-(** [Some b] if locally enabled/disabled according to [b], [None] if
-    we should use the global flag. *)
-type vernac_cumulative = VernacCumulative | VernacNonCumulative
-
 (** {6 The type of vernacular expressions} *)
 
 type vernac_one_argument_status = {
@@ -312,7 +308,7 @@ type nonrec vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of (discharge * Decls.assumption_object_kind) *
       Declaremods.inline * (ident_decl list * constr_expr) with_coercion list
-  | VernacInductive of vernac_cumulative option * bool (* private *) * inductive_kind * (inductive_expr * decl_notation list) list
+  | VernacInductive of inductive_kind * (inductive_expr * decl_notation list) list
   | VernacFixpoint of discharge * fixpoint_expr list
   | VernacCoFixpoint of discharge * cofixpoint_expr list
   | VernacScheme of (lident option * scheme) list
@@ -403,7 +399,7 @@ type nonrec vernac_expr =
   | VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list)
   | VernacSetStrategy of
       (Conv_oracle.level * qualid or_by_notation list) list
-  | VernacSetOption of export_flag * Goptions.option_name * option_setting
+  | VernacSetOption of bool (* Export modifier? *) * Goptions.option_name * option_setting
   | VernacAddOption of Goptions.option_name * option_ref_value list
   | VernacRemoveOption of Goptions.option_name * option_ref_value list
   | VernacMemOption of Goptions.option_name * option_ref_value list