diff options
Diffstat (limited to 'doc')
24 files changed, 209 insertions, 120 deletions
diff --git a/doc/changelog/02-specification-language/13312-attributes+bool_single.rst b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst new file mode 100644 index 0000000000..f069bc616b --- /dev/null +++ b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst @@ -0,0 +1,17 @@ +- **Changed:** + :term:`Boolean attributes <boolean attribute>` are now specified using + key/value pairs, that is to say :n:`@ident__attr{? = {| yes | no } }`. + If the value is missing, the default is :n:`yes`. The old syntax is still + supported, but produces the ``deprecated-attribute-syntax`` warning. + + Deprecated attributes are :attr:`universes(monomorphic)`, + :attr:`universes(notemplate)` and :attr:`universes(noncumulative)`, which are + respectively replaced by :attr:`universes(polymorphic=no) <universes(polymorphic)>`, + :attr:`universes(template=no) <universes(template)>` + and :attr:`universes(cumulative=no) <universes(cumulative)>`. + Attributes :attr:`program` and :attr:`canonical` are also affected, + with the syntax :n:`@ident__attr(false)` being deprecated in favor of + :n:`@ident__attr=no`. + + (`#13312 <https://github.com/coq/coq/pull/13312>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/02-specification-language/13386-master+fix9971-primproj-canonical-structure-on-evar-type.rst b/doc/changelog/02-specification-language/13386-master+fix9971-primproj-canonical-structure-on-evar-type.rst new file mode 100644 index 0000000000..4bd214d7be --- /dev/null +++ b/doc/changelog/02-specification-language/13386-master+fix9971-primproj-canonical-structure-on-evar-type.rst @@ -0,0 +1,6 @@ +- **Fixed:** + issue when two expressions involving different projections and one is + primitive need to be unified + (`#13386 <https://github.com/coq/coq/pull/13386>`_, + fixes `#9971 <https://github.com/coq/coq/issues/9971>`_, + by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst b/doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst new file mode 100644 index 0000000000..e63ab9696e --- /dev/null +++ b/doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Capture of the name of global references by + binders in the presence of notations for binders + (`#12965 <https://github.com/coq/coq/pull/12965>`_, + fixes `#9569 <https://github.com/coq/coq/issues/9569>`_, + by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst b/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst new file mode 100644 index 0000000000..d472e6fdf0 --- /dev/null +++ b/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst @@ -0,0 +1,12 @@ +- **Changed:** + Redeclaring a notation reactivates also its printing rule; in + particular a second :cmd:`Import` of the same module reactivates the + printing rules declared in this module. In theory, this leads to + changes of behavior for printing. However, this is mitigated in + general by the adoption in `#12986 + <https://github.com/coq/coq/pull/12986>`_ of a priority given to + notations which match a larger part of the term to print + (`#12984 <https://github.com/coq/coq/pull/12984>`_, + fixes `#7443 <https://github.com/coq/coq/issues/7443>`_ + and `#10824 <https://github.com/coq/coq/issues/10824>`_, + by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12986-master+ordering-notation-by-precision.rst b/doc/changelog/03-notations/12986-master+ordering-notation-by-precision.rst new file mode 100644 index 0000000000..8b233972bf --- /dev/null +++ b/doc/changelog/03-notations/12986-master+ordering-notation-by-precision.rst @@ -0,0 +1,5 @@ +- **Changed:** + Use of notations for printing now gives preference + to notations which match a larger part of the term to abbreviate + (`#12986 <https://github.com/coq/coq/pull/12986>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst b/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst new file mode 100644 index 0000000000..bc67fd025a --- /dev/null +++ b/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst @@ -0,0 +1,6 @@ +- **Changed:** + Giving an empty list of occurrences after :n:`in` in tactics is no + longer permitted. Omitting the :n:`in` gives the same behavior + (`#13237 <https://github.com/coq/coq/pull/13236>`_, + fixes `#13235 <https://github.com/coq/coq/issues/13235>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13381-bfs_eauto.rst b/doc/changelog/04-tactics/13381-bfs_eauto.rst index a51f96d0a2..f37fbfe52b 100644 --- a/doc/changelog/04-tactics/13381-bfs_eauto.rst +++ b/doc/changelog/04-tactics/13381-bfs_eauto.rst @@ -1,6 +1,6 @@ - **Deprecated:** Undocumented :n:`eauto @int_or_var @int_or_var` syntax in favor of new ``bfs eauto``. - Also deprecated 2-integer syntax for ``debug eauto`` and ``info_eauto``; - replacement TBD. + Also deprecated 2-integer syntax for ``debug eauto`` and ``info_eauto``. + (Use ``bfs eauto`` with the :flag:`Info Eauto` or :flag:`Debug Eauto` flags instead.) (`#13381 <https://github.com/coq/coq/pull/13381>`_, by Jim Fehrle). diff --git a/doc/changelog/04-tactics/13403-occs_nums_nat.rst b/doc/changelog/04-tactics/13403-occs_nums_nat.rst new file mode 100644 index 0000000000..5dfa90a267 --- /dev/null +++ b/doc/changelog/04-tactics/13403-occs_nums_nat.rst @@ -0,0 +1,7 @@ +- **Removed:** + :n:`at @occs_nums` clauses in tactics such as tacn:`unfold` + no longer allow negative values. A "-" before the + list (for set complement) is still supported. Ex: "at -1 -2" + is no longer supported but "at -1 2" is. + (`#13403 <https://github.com/coq/coq/pull/13403>`_, + by Jim Fehrle). 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/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..4615a8dfca 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -122,33 +122,37 @@ 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 :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 ``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`). - 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. +.. attr:: universes(monomorphic) -.. flag:: Universe Polymorphism + .. deprecated:: 8.13 - This flag is off by default. When it is on, new declarations are - polymorphic unless the :attr:`universes(monomorphic)` attribute is - used. + Use :attr:`universes(polymorphic=no) <universes(polymorphic)>` + instead. -.. attr:: universes(monomorphic) - :name: universes(monomorphic); Monomorphic +.. flag:: Universe Polymorphism - 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`). + This flag is off by default. When it is on, new declarations are + polymorphic unless the :attr:`universes(polymorphic=no) <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. @@ -171,19 +175,27 @@ Polymorphism` flag is on or the :attr:`universes(polymorphic)` or 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. - .. exn:: The cumulative and noncumulative attributes can only be used in a polymorphic context. + 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. + + .. 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 @@ -192,26 +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 } }) ]`. -.. flag:: Polymorphic Inductive Cumulativity +.. attr:: universes(noncumulative) - 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. + .. deprecated:: 8.13 -.. attr:: universes(noncumulative) - :name: universes(noncumulative); NonCumulative + Use :attr:`universes(cumulative=no) <universes(cumulative)>` instead. - 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`). +.. flag:: Polymorphic Inductive Cumulativity - This means that two instances of the same inductive type (family) - are convertible only if all the universes are equal. + When this flag is on (it is off by default), it makes all + subsequent *polymorphic* inductive definitions cumulative, unless + the :attr:`universes(cumulative=no) <universes(cumulative)>` attribute is + used to override the default. 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..24fa71059c 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -147,7 +147,7 @@ Specification language, type inference This makes typeclasses with declared modes more robust with respect to the order of resolution. (`#10858 <https://github.com/coq/coq/pull/10858>`_, - fixes `#9058 <https://github.com/coq/coq/issues/9058>_`, by Matthieu Sozeau). + fixes `#9058 <https://github.com/coq/coq/issues/9058>`_, by Matthieu Sozeau). - **Added:** Warn when manual implicit arguments are used in unexpected positions of a term (e.g. in `Check id (forall {x}, x)`) or when an implicit @@ -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 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann). - **Deprecated:** :flag:`Hide Obligations` flag @@ -545,7 +545,7 @@ Flags, options and attributes <https://github.com/coq/coq/pull/11162>`_, 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 <https://github.com/coq/coq/pull/11665>`_, by diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 5406da38a1..2b262b89c0 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 } @@ -379,21 +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. +:gdef:`Boolean attributes <boolean attribute>` 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(monomorphic)` -`Cumulative` :attr:`universes(cumulative)` -`NonCumulative` :attr:`universes(noncumulative)` -`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/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..251b5e4955 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,7 +1056,7 @@ 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)` + This can be prevented using the :attr:`universes(template=no) <universes(template)>` attribute. Template polymorphism and full universe polymorphism (see Chapter @@ -1077,11 +1075,12 @@ 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 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 :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. .. exn:: template and polymorphism not compatible @@ -1094,11 +1093,15 @@ 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. + 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. + .. 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. + .. deprecated:: 8.13 + + Use :attr:`universes(template=no) <universes(template)>` 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 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..f7ce7f1c6c 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -87,29 +87,27 @@ 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) +.. attr:: canonical{? = {| yes | no } } + :name: canonical - 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`). + 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. - .. example:: + 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`). - For instance, when declaring the :g:`Setoid` structure above, the - :g:`Prf_equiv` field declaration could be written as follows. - - .. 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:`hierarchy_of_structures` for a more realistic example. .. cmd:: Print Canonical Projections {* @reference } @@ -248,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 ---------------------------- @@ -331,7 +331,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} _. diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index f3f69a2fdc..5283f60b11 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -274,9 +274,13 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. exn:: Too few occurrences. :undocumented: - .. tacv:: change @term {? {? at {+ @natural}} with @term} in @ident + .. tacv:: change @term {? {? at {+ @natural}} with @term} in @goal_occurrences - This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. + In the presence of :n:`with`, this applies :tacn:`change` to the + occurrences specified by :n:`@goal_occurrences`. In the + absence of :n:`with`, :n:`@goal_occurrences` is expected to + only list hypotheses (and optionally the conclusion) without + specifying occurrences (i.e. no :n:`at` clause). .. tacv:: now_show @term @@ -320,7 +324,7 @@ Performing computations ref_or_pattern_occ ::= @reference {? at @occs_nums } | @one_term {? at @occs_nums } occs_nums ::= {+ {| @natural | @ident } } - | - {| @natural | @ident } {* @int_or_var } + | - {+ {| @natural | @ident } } int_or_var ::= @integer | @ident unfold_occ ::= @reference {? at @occs_nums } diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 56b14d0935..16c8586a9f 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -214,7 +214,7 @@ have to be observed for notations starting with a symbol, e.g., rules starting with “\ ``{``\ ” or “\ ``(``\ ” should be put at level 0. The list of Coq predefined notations can be found in the chapter on :ref:`thecoqlibrary`. -Displaying symbolic notations +Use of notations for printing ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The command :cmd:`Notation` has an effect both on the Coq parser and on the @@ -323,6 +323,26 @@ at the time of use of the notation. scope. Obviously, expressions printed by means of such extra printing rules will not be reparsed to the same form. +.. note:: + + When several notations can be used to print a given term, the + notations which capture the largest subterm of the term are used + preferentially. Here is an example: + + .. coqtop:: in + + Notation "x < y" := (lt x y) (at level 70). + Notation "x < y < z" := (lt x y /\ lt y z) (at level 70, y at next level). + + Check (0 < 1 /\ 1 < 2). + + When several notations match the same subterm, or incomparable + subterms of the term to print, the notation declared most recently + is selected. Moreover, reimporting a library or module declares the + notations of this library or module again. If the notation is in a + scope (see :ref:`Scopes`), either the scope has to be opened or a + delimiter has to exist in the scope for the notation to be usable. + The Infix command ~~~~~~~~~~~~~~~~~~ diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 4c1956d172..816acba4c1 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1939,11 +1939,6 @@ tac2rec_fields: [ | LIST1 tac2rec_field SEP ";" OPT ";" TAG Ltac2 ] -(* todo: weird productions, ints only after an initial "-"??: - occs_nums: [ - | LIST1 [ natural | ident ] - | "-" [ natural | ident ] LIST0 int_or_var -*) ltac2_occs_nums: [ | DELETE LIST1 nat_or_anti (* Ltac2 plugin *) | REPLACE "-" nat_or_anti LIST0 nat_or_anti (* Ltac2 plugin *) diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 033ece04de..03a20d621b 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -480,6 +480,7 @@ opt_hintbases: [ command: [ | "Goal" lconstr | "Proof" +| "Proof" "using" G_vernac.section_subset_expr | "Proof" "Mode" string | "Proof" lconstr | "Abort" @@ -604,7 +605,7 @@ command: [ | "Typeclasses" "Opaque" LIST1 reference | "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT natural | "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ] -| "Proof" "using" G_vernac.section_subset_expr OPT [ "with" Pltac.tactic ] +| "Proof" "using" G_vernac.section_subset_expr "with" Pltac.tactic | "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic | "Print" "Ltac" reference | "Locate" "Ltac" reference @@ -764,6 +765,7 @@ attribute: [ attr_value: [ | "=" string +| "=" IDENT | "(" attribute_list ")" | ] @@ -2327,7 +2329,7 @@ conversion: [ occs_nums: [ | LIST1 nat_or_var -| "-" nat_or_var LIST0 int_or_var +| "-" LIST1 nat_or_var ] occs: [ @@ -2537,6 +2539,7 @@ or_and_intropattern_loc: [ as_or_and_ipat: [ | "as" or_and_intropattern_loc +| "as" equality_intropattern | ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index dfd3a18908..0209cf762a 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -383,6 +383,7 @@ attribute: [ attr_value: [ | "=" string +| "=" ident | "(" LIST0 attribute SEP "," ")" ] @@ -652,7 +653,7 @@ ref_or_pattern_occ: [ occs_nums: [ | LIST1 [ natural | ident ] -| "-" [ natural | ident ] LIST0 int_or_var +| "-" LIST1 [ natural | ident ] ] int_or_var: [ @@ -952,6 +953,7 @@ command: [ | "Extract" "Inductive" qualid "=>" [ ident | string ] "[" LIST0 [ ident | string ] "]" OPT string (* extraction plugin *) | "Show" "Extraction" (* extraction plugin *) | "Proof" +| "Proof" "using" section_var_expr | "Proof" "Mode" string | "Proof" term | "Abort" OPT [ "All" | ident ] @@ -1032,7 +1034,7 @@ command: [ | "Typeclasses" "Opaque" LIST1 qualid | "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" [ "bfs" | "dfs" ] ")" ) OPT natural | "Proof" "with" ltac_expr OPT [ "using" section_var_expr ] -| "Proof" "using" section_var_expr OPT [ "with" ltac_expr ] +| "Proof" "using" section_var_expr "with" ltac_expr | "Tactic" "Notation" OPT ( "(" "at" "level" natural ")" ) LIST1 ltac_production_item ":=" ltac_expr | "Print" "Rewrite" "HintDb" ident | "Print" "Ltac" qualid @@ -1968,6 +1970,7 @@ or_and_intropattern_loc: [ as_or_and_ipat: [ | "as" or_and_intropattern_loc +| "as" equality_intropattern ] eqn_ipat: [ |