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

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

3 files changed, 115 insertions, 86 deletions

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
 ~~~~~~~~~~~~~~~~~~~~~~~