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/language/core/inductive.rst | 24 ++++++++++-------------- 1 file changed, 10 insertions(+), 14 deletions(-) (limited to 'doc/sphinx/language/core/inductive.rst') 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 -- 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/language/core/inductive.rst | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) (limited to 'doc/sphinx/language/core/inductive.rst') 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 -- cgit v1.2.3