From c609c05cf4a5a2a36ca46a0ea890c954d0ae2a5b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 12 Nov 2020 20:21:36 +0100 Subject: [attributes] Deprecate `attr(true)` syntax in favor of booelan attributes. We introduce a warning so boolean attributes are expected to be of the form `attr={yes,no}` or just `attr` (for `yes`). We update the documentation, test-suite, and changelog. --- doc/sphinx/addendum/type-classes.rst | 7 ++-- doc/sphinx/addendum/universe-polymorphism.rst | 54 ++++++++++++--------------- doc/sphinx/changes.rst | 6 +-- doc/sphinx/language/core/basic.rst | 7 +++- doc/sphinx/language/core/coinductive.rst | 6 +-- doc/sphinx/language/core/definitions.rst | 2 +- doc/sphinx/language/core/inductive.rst | 24 +++++------- doc/sphinx/language/core/records.rst | 6 +-- doc/sphinx/language/core/variants.rst | 6 +-- doc/sphinx/language/extensions/canonical.rst | 31 +++++++-------- 10 files changed, 66 insertions(+), 83 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 2474c784b8..22527dc379 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -320,10 +320,9 @@ Summary of the commands maintained. Like any command declaring a record, this command supports the - :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, - :attr:`universes(template)`, :attr:`universes(notemplate)`, - :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and - :attr:`private(matching)` attributes. + :attr:`universes(polymorphic)`, :attr:`universes(template)`, + :attr:`universes(cumulative)`, and :attr:`private(matching)` + attributes. .. cmd:: Existing Class @qualid diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 064107d088..a2ed23335e 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -125,30 +125,27 @@ Polymorphic, Monomorphic .. attr:: universes(polymorphic) :name: universes(polymorphic); Polymorphic - This attribute can be used to declare universe polymorphic - definitions and inductive types. There is also a legacy syntax - using the ``Polymorphic`` prefix (see :n:`@legacy_attr`) which, as - shown in the examples, is more commonly used. + This boolean attribute can be used to control whether universe + polymorphism is enabled in the definition of an inductive type. + There is also a legacy syntax using the ``Polymorphic`` prefix (see + :n:`@legacy_attr`) which, as shown in the examples, is more + commonly used. + + When ``polymorphic=no`` is set, global universe constraints + are produced, even when the :flag:`Universe Polymorphism` flag is + on. There is also a legacy syntax using the ``Monomorphic`` prefix + (see :n:`@legacy_attr`). .. flag:: Universe Polymorphism This flag is off by default. When it is on, new declarations are - polymorphic unless the :attr:`universes(monomorphic)` attribute is - used. - -.. attr:: universes(monomorphic) - :name: universes(monomorphic); Monomorphic - - This attribute can be used to declare universe monomorphic - definitions and inductive types (i.e. global universe constraints - are produced), even when the :flag:`Universe Polymorphism` flag is - on. There is also a legacy syntax using the ``Monomorphic`` prefix - (see :n:`@legacy_attr`). + polymorphic unless the :attr:`universes(polymorphic)` attribute is + used to override the default. Many other commands can be used to declare universe polymorphic or monomorphic constants depending on whether the :flag:`Universe -Polymorphism` flag is on or the :attr:`universes(polymorphic)` or -:attr:`universes(monomorphic)` attributes are used: +Polymorphism` flag is on or the :attr:`universes(polymorphic)` +attribute is used: - :cmd:`Lemma`, :cmd:`Axiom`, etc. can be used to declare universe polymorphic constants. @@ -183,6 +180,9 @@ Cumulative, NonCumulative are convertible based on the universe variances; they do not need to be equal. + This means that two instances of the same inductive type (family) + are convertible only if all the universes are equal. + .. exn:: The cumulative and noncumulative attributes can only be used in a polymorphic context. Using this attribute requires being in a polymorphic context, @@ -195,23 +195,17 @@ Cumulative, NonCumulative ``#[ universes(polymorphic), universes(cumulative) ]`` can be abbreviated into ``#[ universes(polymorphic, cumulative) ]``. + When the attribtue is off, the inductive type as non-cumulative + even if the :flag:`Polymorphic Inductive Cumulativity` flag is on. + There is also a legacy syntax using the ``NonCumulative`` prefix + (see :n:`@legacy_attr`). + .. flag:: Polymorphic Inductive Cumulativity When this flag is on (it is off by default), it makes all subsequent *polymorphic* inductive definitions cumulative, unless - the :attr:`universes(noncumulative)` attribute is used. It has no - effect on *monomorphic* inductive definitions. - -.. attr:: universes(noncumulative) - :name: universes(noncumulative); NonCumulative - - Declares the inductive type as non-cumulative even if the - :flag:`Polymorphic Inductive Cumulativity` flag is on. There is - also a legacy syntax using the ``NonCumulative`` prefix (see - :n:`@legacy_attr`). - - This means that two instances of the same inductive type (family) - are convertible only if all the universes are equal. + the :attr:`universes(cumulative)` attribute with setting ``off`` is + used. It has no effect on *monomorphic* inductive definitions. Consider the examples below. diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index de5dbe79cc..4d59fc0513 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -533,8 +533,8 @@ Flags, options and attributes - **Removed:** Unqualified ``polymorphic``, ``monomorphic``, ``template``, ``notemplate`` attributes (they were deprecated since Coq 8.10). - Use :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, - :attr:`universes(template)` and :attr:`universes(notemplate)` instead + Use :attr:`universes(polymorphic)`, ``universes(monomorphic)``, + :attr:`universes(template)` and ``universes(notemplate)`` instead (`#11663 `_, by Théo Zimmermann). - **Deprecated:** :flag:`Hide Obligations` flag @@ -545,7 +545,7 @@ Flags, options and attributes `_, by Enrico Tassi). - **Added:** New attributes supported when defining an inductive type - :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and + :attr:`universes(cumulative)`, ``universes(noncumulative)`` and :attr:`private(matching)`, which correspond to legacy attributes ``Cumulative``, ``NonCumulative``, and the previously undocumented ``Private`` (`#11665 `_, by diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 5406da38a1..af5c47dba8 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -379,6 +379,9 @@ this attribute`. The order of top-level attributes doesn't affect their meaning. ``#[foo,bar]``, ``#[bar,foo]``, ``#[foo]#[bar]`` and ``#[bar]#[foo]`` are equivalent. +Boolean attributes take the form ``attr={yes,no}``, when the key is +omitted the default is assumed to be ``yes``. + The legacy attributes (:n:`@legacy_attr`) provide an older, alternate syntax for certain attributes. They are equivalent to new attributes as follows: @@ -388,9 +391,9 @@ Legacy attribute New attribute `Local` :attr:`local` `Global` :attr:`global` `Polymorphic` :attr:`universes(polymorphic)` -`Monomorphic` :attr:`universes(monomorphic)` +`Monomorphic` :attr:`universes(polymorphic)` `Cumulative` :attr:`universes(cumulative)` -`NonCumulative` :attr:`universes(noncumulative)` +`NonCumulative` :attr:`universes(cumulative)` `Private` :attr:`private(matching)` `Program` :attr:`program` ================ ================================ diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst index 3e2ecdc0f0..43bbc8b40d 100644 --- a/doc/sphinx/language/core/coinductive.rst +++ b/doc/sphinx/language/core/coinductive.rst @@ -26,10 +26,8 @@ More information on co-inductive definitions can be found in For co-inductive types, the only elimination principle is case analysis. This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`universes(template)`, - :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)`, :attr:`private(matching)` - and :attr:`using` attributes. + :attr:`universes(template)`, :attr:`universes(cumulative)`, + :attr:`private(matching)`, and :attr:`using` attributes. .. example:: diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 79489c85f6..57771c9036 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -90,7 +90,7 @@ Section :ref:`typing-rules`. computation on :n:`@term`. These commands also support the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`program` (see :ref:`program_definition`), + :attr:`program` (see :ref:`program_definition`), :attr:`canonical` and :attr:`using` attributes. If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index ad7d6f3963..b9453650eb 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -32,10 +32,8 @@ Inductive types proposition). This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`universes(template)`, - :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)` and :attr:`private(matching)` - attributes. + :attr:`universes(template)`, :attr:`universes(cumulative)`, and + :attr:`private(matching)` attributes. Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s. The :n:`@ident`\s are simultaneously added to the environment before the types of constructors are checked. @@ -1058,8 +1056,8 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or at level :math:`\Type` (without annotations or hiding it behind a definition) template polymorphic if possible. - This can be prevented using the :attr:`universes(notemplate)` - attribute. + This can be prevented using the :attr:`universes(template)` + attribute with the ``=no`` setting. Template polymorphism and full universe polymorphism (see Chapter :ref:`polymorphicuniverses`) are incompatible, so if the latter is @@ -1079,9 +1077,9 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or .. attr:: universes(template) - This attribute can be used to explicitly declare an inductive type - as template polymorphic, whether the :flag:`Auto Template - Polymorphism` flag is on or off. + This boolean attribute can be used to explicitly declare an + inductive type as template polymorphic, whether the :flag:`Auto + Template Polymorphism` flag is on or off. .. exn:: template and polymorphism not compatible @@ -1094,11 +1092,9 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or The attribute was used but the inductive definition does not satisfy the criterion to be template polymorphic. -.. attr:: universes(notemplate) - - This attribute can be used to prevent an inductive type to be - template polymorphic, even if the :flag:`Auto Template - Polymorphism` flag is on. + When ``universes(template=no)`` is used, it will prevent an + inductive type to be template polymorphic, even if the :flag:`Auto + Template Polymorphism` flag is on. In practice, the rule **Ind-Family** is used by Coq only when all the inductive types of the inductive definition are declared with an arity diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index e6df3ee9f5..7eedbcd59a 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -53,10 +53,8 @@ expressions. In this sense, the :cmd:`Record` construction allows defining :cmd:`Record` and :cmd:`Structure` are synonyms. This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`universes(template)`, - :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)` and :attr:`private(matching)` - attributes. + :attr:`universes(template)`, :attr:`universes(cumulative)`, and + :attr:`private(matching)` attributes. More generally, a record may have explicitly defined (a.k.a. manifest) fields. For instance, we might have: diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst index 645986be9c..6ac6626dbe 100644 --- a/doc/sphinx/language/core/variants.rst +++ b/doc/sphinx/language/core/variants.rst @@ -17,10 +17,8 @@ Variants this variant, unless the :flag:`Nonrecursive Elimination Schemes` flag is on. This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`universes(template)`, - :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)` and :attr:`private(matching)` - attributes. + :attr:`universes(template)`, :attr:`universes(cumulative)`, and + :attr:`private(matching)` attributes. .. exn:: The @natural th argument of @ident must be @ident in @type. :undocumented: diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index 48120503af..ec3e3e8aa6 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -87,29 +87,26 @@ in :ref:`canonicalstructures`; here only a simple example is given. If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered. - .. attr:: canonical(false) - - To prevent a field from being involved in the inference of - canonical instances, its declaration can be annotated with the - :attr:`canonical(false)` attribute (cf. the syntax of - :n:`@record_field`). +.. attr:: canonical - .. example:: + This boolean attribute can decorate a :cmd:`Definition` or + :cmd:`Let` command. It is equivalent to having a :cmd:`Canonical + Structure` declaration just after the command. - For instance, when declaring the :g:`Setoid` structure above, the - :g:`Prf_equiv` field declaration could be written as follows. + To prevent a field from being involved in the inference of + canonical instances, its declaration can be annotated with + ``canonical=no`` (cf. the syntax of :n:`@record_field`). - .. coqdoc:: + .. example:: - #[canonical(false)] Prf_equiv : equivalence Carrier Equal + For instance, when declaring the :g:`Setoid` structure above, the + :g:`Prf_equiv` field declaration could be written as follows. - See :ref:`canonicalstructures` for a more realistic example. + .. coqdoc:: -.. attr:: canonical + #[canonical=no] Prf_equiv : equivalence Carrier Equal - This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command. - It is equivalent to having a :cmd:`Canonical Structure` declaration just - after the command. + See :ref:`canonicalstructures` for a more realistic example. .. cmd:: Print Canonical Projections {* @reference } @@ -331,7 +328,7 @@ We need to define a new class that inherits from both ``EQ`` and ``LE``. LE_class : LE.class T; extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }. - Structure type := _Pack { obj : Type; #[canonical(false)] class_of : class obj }. + Structure type := _Pack { obj : Type; #[canonical=no] class_of : class obj }. Arguments Mixin {e le} _. -- cgit v1.2.3 From 3b479357d8c5c1a655b2b8257f14a8cafe7621fc Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Sat, 14 Nov 2020 16:01:00 +0100 Subject: Run doc_grammar for #13312. --- doc/sphinx/language/core/basic.rst | 1 + 1 file changed, 1 insertion(+) (limited to 'doc/sphinx') diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index af5c47dba8..ea29da6dd4 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -369,6 +369,7 @@ this attribute`. attributes ::= {* #[ {*, @attribute } ] } {* @legacy_attr } attribute ::= @ident {? @attr_value } attr_value ::= = @string + | = @ident | ( {*, @attribute } ) legacy_attr ::= {| Local | Global } | {| Polymorphic | Monomorphic } -- cgit v1.2.3 From ca42305f1ed1699065cffdef7d96bf5fcc0069be Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Sat, 14 Nov 2020 18:44:57 +0100 Subject: Review commit: improving the doc of boolean attributes. --- doc/sphinx/addendum/program.rst | 8 ++--- doc/sphinx/addendum/universe-polymorphism.rst | 49 +++++++++++++++++---------- doc/sphinx/language/core/basic.rst | 26 +++++++------- doc/sphinx/language/core/inductive.rst | 15 +++++--- doc/sphinx/language/extensions/canonical.rst | 7 ++-- 5 files changed, 63 insertions(+), 42 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 298ea4b4ab..104f84a253 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -99,15 +99,15 @@ coercions. Enables the program mode, in which 1) typechecking allows subset coercions and 2) the elaboration of pattern matching of :cmd:`Fixpoint` and - :cmd:`Definition` act as if the :attr:`program` attribute had been + :cmd:`Definition` acts as if the :attr:`program` attribute has been used, generating obligations if there are unresolved holes after typechecking. -.. attr:: program +.. attr:: program{? = {| yes | no } } :name: program; Program - Allows using the Program mode on a specific - definition. An alternative syntax is to use the legacy ``Program`` + This :term:`boolean attribute` allows using or disabling the Program mode on a specific + definition. An alternative and commonly used syntax is to use the legacy ``Program`` prefix (cf. :n:`@legacy_attr`) as it is elsewhere in this chapter. .. _syntactic_control: diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index a2ed23335e..3790f36e5a 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -122,25 +122,32 @@ in a universe strictly higher than :g:`Set`. Polymorphic, Monomorphic ------------------------- -.. attr:: universes(polymorphic) - :name: universes(polymorphic); Polymorphic +.. attr:: universes(polymorphic{? = {| yes | no } }) + :name: universes(polymorphic); Polymorphic; Monomorphic - This boolean attribute can be used to control whether universe + This :term:`boolean attribute` can be used to control whether universe polymorphism is enabled in the definition of an inductive type. There is also a legacy syntax using the ``Polymorphic`` prefix (see :n:`@legacy_attr`) which, as shown in the examples, is more commonly used. - When ``polymorphic=no`` is set, global universe constraints + When ``universes(polymorphic=no)`` is used, global universe constraints are produced, even when the :flag:`Universe Polymorphism` flag is on. There is also a legacy syntax using the ``Monomorphic`` prefix (see :n:`@legacy_attr`). +.. attr:: universes(monomorphic) + + .. deprecated:: 8.13 + + Use :attr:`universes(polymorphic=no) ` + instead. + .. flag:: Universe Polymorphism This flag is off by default. When it is on, new declarations are - polymorphic unless the :attr:`universes(polymorphic)` attribute is - used to override the default. + polymorphic unless the :attr:`universes(polymorphic=no) ` + attribute is used to override the default. Many other commands can be used to declare universe polymorphic or monomorphic constants depending on whether the :flag:`Universe @@ -168,18 +175,23 @@ attribute is used: Cumulative, NonCumulative ------------------------- -.. attr:: universes(cumulative) - :name: universes(cumulative); Cumulative +.. attr:: universes(cumulative{? = {| yes | no } }) + :name: universes(cumulative); Cumulative; NonCumulative Polymorphic inductive types, coinductive types, variants and - records can be declared cumulative using this attribute or the - legacy ``Cumulative`` prefix (see :n:`@legacy_attr`) which, as + records can be declared cumulative using this :term:`boolean attribute` + or the legacy ``Cumulative`` prefix (see :n:`@legacy_attr`) which, as shown in the examples, is more commonly used. This means that two instances of the same inductive type (family) are convertible based on the universe variances; they do not need to be equal. + When the attribtue is off, the inductive type is non-cumulative + even if the :flag:`Polymorphic Inductive Cumulativity` flag is on. + There is also a legacy syntax using the ``NonCumulative`` prefix + (see :n:`@legacy_attr`). + This means that two instances of the same inductive type (family) are convertible only if all the universes are equal. @@ -192,20 +204,21 @@ Cumulative, NonCumulative .. note:: - ``#[ universes(polymorphic), universes(cumulative) ]`` can be - abbreviated into ``#[ universes(polymorphic, cumulative) ]``. + :n:`#[ universes(polymorphic{? = yes }), universes(cumulative{? = {| yes | no } }) ]` can be + abbreviated into :n:`#[ universes(polymorphic{? = yes }, cumulative{? = {| yes | no } }) ]`. - When the attribtue is off, the inductive type as non-cumulative - even if the :flag:`Polymorphic Inductive Cumulativity` flag is on. - There is also a legacy syntax using the ``NonCumulative`` prefix - (see :n:`@legacy_attr`). +.. attr:: universes(noncumulative) + + .. deprecated:: 8.13 + + Use :attr:`universes(cumulative=no) ` instead. .. flag:: Polymorphic Inductive Cumulativity When this flag is on (it is off by default), it makes all subsequent *polymorphic* inductive definitions cumulative, unless - the :attr:`universes(cumulative)` attribute with setting ``off`` is - used. It has no effect on *monomorphic* inductive definitions. + the :attr:`universes(cumulative=no) ` attribute is + used to override the default. It has no effect on *monomorphic* inductive definitions. Consider the examples below. diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index ea29da6dd4..2b262b89c0 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -380,24 +380,22 @@ this attribute`. The order of top-level attributes doesn't affect their meaning. ``#[foo,bar]``, ``#[bar,foo]``, ``#[foo]#[bar]`` and ``#[bar]#[foo]`` are equivalent. -Boolean attributes take the form ``attr={yes,no}``, when the key is -omitted the default is assumed to be ``yes``. +:gdef:`Boolean attributes ` take the form :n:`@ident__attr{? = {| yes | no } }`. +When the :n:`{| yes | no }` value is omitted, the default is :n:`yes`. The legacy attributes (:n:`@legacy_attr`) provide an older, alternate syntax for certain attributes. They are equivalent to new attributes as follows: -================ ================================ -Legacy attribute New attribute -================ ================================ -`Local` :attr:`local` -`Global` :attr:`global` -`Polymorphic` :attr:`universes(polymorphic)` -`Monomorphic` :attr:`universes(polymorphic)` -`Cumulative` :attr:`universes(cumulative)` -`NonCumulative` :attr:`universes(cumulative)` -`Private` :attr:`private(matching)` -`Program` :attr:`program` -================ ================================ +============================= ================================ +Legacy attribute New attribute +============================= ================================ +`Local` :attr:`local` +`Global` :attr:`global` +`Polymorphic`, `Monomorphic` :attr:`universes(polymorphic)` +`Cumulative`, `NonCumulative` :attr:`universes(cumulative)` +`Private` :attr:`private(matching)` +`Program` :attr:`program` +============================= ================================ Attributes appear in the HTML documentation in blue or gray boxes after the label "Attribute". In the pdf, they appear after the diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index b9453650eb..251b5e4955 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -1056,8 +1056,8 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or at level :math:`\Type` (without annotations or hiding it behind a definition) template polymorphic if possible. - This can be prevented using the :attr:`universes(template)` - attribute with the ``=no`` setting. + This can be prevented using the :attr:`universes(template=no) ` + attribute. Template polymorphism and full universe polymorphism (see Chapter :ref:`polymorphicuniverses`) are incompatible, so if the latter is @@ -1075,9 +1075,10 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or the :attr:`universes(template)` attribute: in this case, the warning is not emitted. -.. attr:: universes(template) +.. attr:: universes(template{? = {| yes | no } }) + :name: universes(template) - This boolean attribute can be used to explicitly declare an + This :term:`boolean attribute` can be used to explicitly declare an inductive type as template polymorphic, whether the :flag:`Auto Template Polymorphism` flag is on or off. @@ -1096,6 +1097,12 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or inductive type to be template polymorphic, even if the :flag:`Auto Template Polymorphism` flag is on. +.. attr:: universes(notemplate) + + .. deprecated:: 8.13 + + Use :attr:`universes(template=no) ` instead. + In practice, the rule **Ind-Family** is used by Coq only when all the inductive types of the inductive definition are declared with an arity whose sort is in the Type hierarchy. Then, the polymorphism is over diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index ec3e3e8aa6..f7ce7f1c6c 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -87,7 +87,8 @@ in :ref:`canonicalstructures`; here only a simple example is given. If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered. -.. attr:: canonical +.. attr:: canonical{? = {| yes | no } } + :name: canonical This boolean attribute can decorate a :cmd:`Definition` or :cmd:`Let` command. It is equivalent to having a :cmd:`Canonical @@ -106,7 +107,7 @@ in :ref:`canonicalstructures`; here only a simple example is given. #[canonical=no] Prf_equiv : equivalence Carrier Equal - See :ref:`canonicalstructures` for a more realistic example. + See :ref:`hierarchy_of_structures` for a more realistic example. .. cmd:: Print Canonical Projections {* @reference } @@ -245,6 +246,8 @@ for each component of the pair. The declaration associates to the key ``*`` relation ``pair_eq`` whenever the type constructor ``*`` is applied to two types being themselves in the ``EQ`` class. +.. _hierarchy_of_structures: + Hierarchy of structures ---------------------------- -- cgit v1.2.3 From 6aeee2e4e37d4b8ffb8c50c109903ad336c8bdfa Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 15 Nov 2020 15:57:37 +0100 Subject: [attributes] Update error message referring to deprecated syntax. --- doc/sphinx/addendum/universe-polymorphism.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 3790f36e5a..4615a8dfca 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -195,7 +195,7 @@ Cumulative, NonCumulative This means that two instances of the same inductive type (family) are convertible only if all the universes are equal. - .. exn:: The cumulative and noncumulative attributes can only be used in a polymorphic context. + .. exn:: The cumulative attribute can only be used in a polymorphic context. Using this attribute requires being in a polymorphic context, i.e. either having the :flag:`Universe Polymorphism` flag on, or -- cgit v1.2.3