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

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

3 files changed, 131 insertions, 148 deletions

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