diff options
Diffstat (limited to 'doc')
170 files changed, 1968 insertions, 1514 deletions
diff --git a/doc/README.md b/doc/README.md index 79d1e1b756..440b104c16 100644 --- a/doc/README.md +++ b/doc/README.md @@ -69,6 +69,16 @@ Or if you want to use less disk space: apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \ latexmk fonts-freefont-otf +### Setting the locale for Python + +Make sure that the locale is configured on your platform so that Python encodes +printed messages with utf-8 rather than generating runtime exceptions +for non-ascii characters. The `.UTF-8` in `export LANG=C.UTF-8` sets UTF-8 encoding. +The `C` can be replaced with any supported language code. You can set the default +for a Docker build with `ENV LANG C.UTF-8`. (Python may look at other +environment variables to determine the locale; see the +[Python documentation](https://docs.python.org/3/library/locale.html#locale.getdefaultlocale)). + Compilation ----------- diff --git a/doc/changelog/01-kernel/00000-title.rst b/doc/changelog/01-kernel/00000-title.rst index f680628a05..287382eab0 100644 --- a/doc/changelog/01-kernel/00000-title.rst +++ b/doc/changelog/01-kernel/00000-title.rst @@ -1,3 +1,4 @@ -**Kernel** +Kernel +^^^^^^ diff --git a/doc/changelog/01-kernel/10390-uip.rst b/doc/changelog/01-kernel/10390-uip.rst deleted file mode 100644 index dab096d8db..0000000000 --- a/doc/changelog/01-kernel/10390-uip.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Definitional UIP, only when :flag:`Definitional UIP` is enabled. See - documentation of the flag for details. - (`#10390 <https://github.com/coq/coq/pull/10390>`_, - by Gaëtan Gilbert). diff --git a/doc/changelog/01-kernel/11604-persistent-arrays.rst b/doc/changelog/01-kernel/11604-persistent-arrays.rst deleted file mode 100644 index fbade033d2..0000000000 --- a/doc/changelog/01-kernel/11604-persistent-arrays.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - Built-in support for persistent arrays, which expose a functional - interface but are implemented using an imperative data structure, for - better performance. - (`#11604 <https://github.com/coq/coq/pull/11604>`_, - by Maxime Dénès and Benjamin Grégoire, with help from Gaëtan Gilbert). diff --git a/doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst b/doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst deleted file mode 100644 index bec121836c..0000000000 --- a/doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Fixed:** - A loss of definitional equality for declarations obtained through - :cmd:`Include` when entering the scope of a :cmd:`Module` or - :cmd:`Module Type` was causing :cmd:`Search` not to see the included - declarations - (`#12537 <https://github.com/coq/coq/pull/12537>`_, fixes `#12525 - <https://github.com/coq/coq/pull/12525>`_ and `#12647 - <https://github.com/coq/coq/pull/12647>`_, by Hugo Herbelin). diff --git a/doc/changelog/01-kernel/13356-primarray-cumul.rst b/doc/changelog/01-kernel/13356-primarray-cumul.rst deleted file mode 100644 index 978ca325bf..0000000000 --- a/doc/changelog/01-kernel/13356-primarray-cumul.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** Primitive arrays are now irrelevant in their single - polymorphic universe (same as a polymorphic cumulative list - inductive would be) (`#13356 - <https://github.com/coq/coq/pull/13356>`_, fixes `#13354 - <https://github.com/coq/coq/issues/13354>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/01-kernel/13501-fix-13495.rst b/doc/changelog/01-kernel/13501-fix-13495.rst deleted file mode 100644 index 5c81efa8b9..0000000000 --- a/doc/changelog/01-kernel/13501-fix-13495.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Fixed:** - Fix an incompleteness in the typechecking of `match` for - cumulative inductive types. This could result in breaking subject - reduction. - (`#13501 <https://github.com/coq/coq/pull/13501>`_, - fixes `#13495 <https://github.com/coq/coq/issues/13495>`_, - by Matthieu Sozeau). diff --git a/doc/changelog/01-kernel/13563-compact-case-repr.rst b/doc/changelog/01-kernel/13563-compact-case-repr.rst new file mode 100644 index 0000000000..c8ee9bc1e6 --- /dev/null +++ b/doc/changelog/01-kernel/13563-compact-case-repr.rst @@ -0,0 +1,15 @@ +- **Changed:** + The term representation of pattern-matchings now uses a compact form that + provides a few static guarantees such as eta-expansion of branches and return + clauses and is usually more efficient. The most visible user change is that for + the time being, the :tacn:`destruct` tactic and its variants generate dummy + cuts (β redexes) in the branches of the generated proof. + This can also generate very uncommon backwards incompatibilities, such as a + change of occurrence numbering for subterms, or breakage of unification in + complex situations involving pattern-matchings whose underlying inductive type + declares let-bindings in parameters, arity or constructor types. For ML plugin + developers, an in-depth description of the new representation, as well as + porting tips, can be found in dev/doc/case-repr.md + (`#13563 <https://github.com/coq/coq/pull/13563>`_, + fixes `#3166 <https://github.com/coq/coq/issues/3166>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/02-specification-language/00000-title.rst b/doc/changelog/02-specification-language/00000-title.rst index 99bd2c5b44..2d3e49a69d 100644 --- a/doc/changelog/02-specification-language/00000-title.rst +++ b/doc/changelog/02-specification-language/00000-title.rst @@ -1,3 +1,4 @@ -**Specification language, type inference** +Specification language, type inference +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/doc/changelog/02-specification-language/07825-rechable-from-evars.rst b/doc/changelog/02-specification-language/07825-rechable-from-evars.rst deleted file mode 100644 index e57d5a7bc5..0000000000 --- a/doc/changelog/02-specification-language/07825-rechable-from-evars.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Changed:** - In :tacn:`refine`, new existential variables unified with existing ones are no - longer considered as fresh. The behavior of :tacn:`simple refine` no longer depends on - the orientation of evar-evar unification problems, and new existential variables - are always turned into (unshelved) goals. This can break compatibility in - some cases (`#7825 <https://github.com/coq/coq/pull/7825>`_, by Matthieu - Sozeau, with help from Maxime Dénès, review by Pierre-Marie Pédrot and - Enrico Tassi, fixes `#4095 <https://github.com/coq/coq/issues/4095>`_ and - `#4413 <https://github.com/coq/coq/issues/4413>`_). diff --git a/doc/changelog/02-specification-language/10331-minim-prop-toset.rst b/doc/changelog/02-specification-language/10331-minim-prop-toset.rst deleted file mode 100644 index 6c442ca1aa..0000000000 --- a/doc/changelog/02-specification-language/10331-minim-prop-toset.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** Heuristics for universe minimization to :g:`Set`: also - use constraints ``Prop <= i`` (`#10331 - <https://github.com/coq/coq/pull/10331>`_, by Gaëtan Gilbert with - help from Maxime Dénès and Matthieu Sozeau, fixes `#12414 - <https://github.com/coq/coq/issues/12414>`_). diff --git a/doc/changelog/02-specification-language/12653-cumul-syntax.rst b/doc/changelog/02-specification-language/12653-cumul-syntax.rst deleted file mode 100644 index ba97f7c796..0000000000 --- a/doc/changelog/02-specification-language/12653-cumul-syntax.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** Commands :cmd:`Inductive`, :cmd:`Record` and synonyms now - support syntax `Inductive foo@{=i +j *k l}` to specify variance - information for their universes (in :ref:`Cumulative <cumulative>` - mode) (`#12653 <https://github.com/coq/coq/pull/12653>`_, by Gaëtan - Gilbert). diff --git a/doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst b/doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst deleted file mode 100644 index b0cf4ca4e3..0000000000 --- a/doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Changed:** - Tweaked the algorithm giving default names to arguments. - Should reduce the frequency that argument names get an - unexpected suffix. - Also makes :flag:`Mangle Names` not mess up argument names. - (`#12756 <https://github.com/coq/coq/pull/12756>`_, - fixes `#12001 <https://github.com/coq/coq/issues/12001>`_ - and `#6785 <https://github.com/coq/coq/issues/6785>`_, - by Jasper Hugunin). diff --git a/doc/changelog/02-specification-language/12768-master+warn-non-underscore-catch-all-pattern-matching.rst b/doc/changelog/02-specification-language/12768-master+warn-non-underscore-catch-all-pattern-matching.rst deleted file mode 100644 index c9e941743c..0000000000 --- a/doc/changelog/02-specification-language/12768-master+warn-non-underscore-catch-all-pattern-matching.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Added:** - Warning on unused variables in pattern-matching branches of - :n:`match` serving as catch-all branches for at least two distinct - patterns. - (`#12768 <https://github.com/coq/coq/pull/12768>`_, - fixes `#12762 <https://github.com/coq/coq/issues/12762>`_, - by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/13106-doc-and-changelog-for-13106.rst b/doc/changelog/02-specification-language/13106-doc-and-changelog-for-13106.rst deleted file mode 100644 index 7fe69c39c1..0000000000 --- a/doc/changelog/02-specification-language/13106-doc-and-changelog-for-13106.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Removed:** - Undocumented and experimental forward class hint feature ``:>>``. - Use ``:>`` (see :n:`@of_type`) instead - (`#13106 <https://github.com/coq/coq/pull/13106>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst b/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst deleted file mode 100644 index 006989e6b3..0000000000 --- a/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Implicit arguments taken into account in defined fields of a record type declaration - (`#13166 <https://github.com/coq/coq/pull/13166>`_, - fixes `#13165 <https://github.com/coq/coq/issues/13165>`_, - by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/13183-using-att.rst b/doc/changelog/02-specification-language/13183-using-att.rst deleted file mode 100644 index c380d932ed..0000000000 --- a/doc/changelog/02-specification-language/13183-using-att.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - Definition and (Co)Fixpoint now support the :attr:`using` attribute. - It has the same effect as :cmd:`Proof using`, which is only available in - interactive mode. - (`#13183 <https://github.com/coq/coq/pull/13183>`_, - by Enrico Tassi). diff --git a/doc/changelog/02-specification-language/13188-instance-gen.rst b/doc/changelog/02-specification-language/13188-instance-gen.rst deleted file mode 100644 index 6a431f85ed..0000000000 --- a/doc/changelog/02-specification-language/13188-instance-gen.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Removed:** The type given to :cmd:`Instance` is no longer automatically - generalized over unbound and :ref:`generalizable <implicit-generalization>` variables. - Use :n:`Instance : \`{@type}` instead of :n:`Instance : @type` to get the old behaviour, or - enable the compatibility flag :flag:`Instance Generalized Output`. - (`#13188 <https://github.com/coq/coq/pull/13188>`_, fixes `#6042 - <https://github.com/coq/coq/issues/6042>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/13217-master+fix13216-typeclass-for-match-return-clause.rst b/doc/changelog/02-specification-language/13217-master+fix13216-typeclass-for-match-return-clause.rst deleted file mode 100644 index 2d8230b965..0000000000 --- a/doc/changelog/02-specification-language/13217-master+fix13216-typeclass-for-match-return-clause.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Allow use of type classes inference for the return predicate of a :n:`match` - (was deactivated in versions 8.10 to 8.12, `#13217 <https://github.com/coq/coq/pull/13217>`_, - fixes `#13216 <https://github.com/coq/coq/issues/13216>`_, - by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst b/doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst deleted file mode 100644 index bf792fda6d..0000000000 --- a/doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - Inference of return predicate of a :g:`match` by inversion takes - sort elimination constraints into account - (`#13290 <https://github.com/coq/coq/pull/13290>`_, - grants `#13278 <https://github.com/coq/coq/issues/13278>`_, - by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/13312-attributes+bool_single.rst b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst deleted file mode 100644 index f069bc616b..0000000000 --- a/doc/changelog/02-specification-language/13312-attributes+bool_single.rst +++ /dev/null @@ -1,17 +0,0 @@ -- **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/13376-master+minifix-NotFoundInstance.rst b/doc/changelog/02-specification-language/13376-master+minifix-NotFoundInstance.rst deleted file mode 100644 index 5758f35c3d..0000000000 --- a/doc/changelog/02-specification-language/13376-master+minifix-NotFoundInstance.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - A case of unification raising an anomaly IllTypedInstance - (`#13376 <https://github.com/coq/coq/pull/13376>`_, - fixes `#13266 <https://github.com/coq/coq/issues/13266>`_, - by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/13383-master+fix11816-wf-not-allowed-in-local-fixpoint.rst b/doc/changelog/02-specification-language/13383-master+fix11816-wf-not-allowed-in-local-fixpoint.rst deleted file mode 100644 index c0e5a81641..0000000000 --- a/doc/changelog/02-specification-language/13383-master+fix11816-wf-not-allowed-in-local-fixpoint.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Using :n:`{wf ...}` in local fixpoints is an error, not an anomaly - (`#13383 <https://github.com/coq/coq/pull/13383>`_, - fixes `#11816 <https://github.com/coq/coq/issues/11816>`_, - by Hugo Herbelin). 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 deleted file mode 100644 index 4bd214d7be..0000000000 --- a/doc/changelog/02-specification-language/13386-master+fix9971-primproj-canonical-structure-on-evar-type.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **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/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst b/doc/changelog/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst deleted file mode 100644 index eaf049dc97..0000000000 --- a/doc/changelog/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - A bug producing ill-typed instances of existential variables when let-ins - interleaved with assumptions - (`#13387 <https://github.com/coq/coq/pull/13387>`_, - fixes `#12348 <https://github.com/coq/coq/issues/13387>`_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/00000-title.rst b/doc/changelog/03-notations/00000-title.rst index abc532df11..0780bf9468 100644 --- a/doc/changelog/03-notations/00000-title.rst +++ b/doc/changelog/03-notations/00000-title.rst @@ -1,3 +1,4 @@ -**Notations** +Notations +^^^^^^^^^ diff --git a/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst b/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst deleted file mode 100644 index 8d681361e8..0000000000 --- a/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst +++ /dev/null @@ -1,13 +0,0 @@ -- **Changed:** - In notations (except in custom entries), the misleading :n:`@syntax_modifier` - :n:`@ident ident` (which accepted either an identifier or - a :g:`_`) is deprecated and should be replaced by :n:`@ident name`. If - the intent was really to only parse identifiers, this will - eventually become possible, but only as of Coq 8.15. - In custom entries, the meaning of :n:`@ident ident` is silently changed - from parsing identifiers or :g:`_` to parsing only identifiers - without warning, but this presumably affects only rare, recent and - relatively experimental code - (`#11841 <https://github.com/coq/coq/pull/11841>`_, - fixes `#9514 <https://github.com/coq/coq/pull/9514>`_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/11986-float-low-level-printing.rst b/doc/changelog/03-notations/11986-float-low-level-printing.rst deleted file mode 100644 index aba74891c6..0000000000 --- a/doc/changelog/03-notations/11986-float-low-level-printing.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - :flag:`Printing Float` flag to print primitive floats as hexadecimal - instead of decimal values. This is included in the :flag:`Printing All` flag - (`#11986 <https://github.com/coq/coq/pull/11986>`_, - by Pierre Roux). diff --git a/doc/changelog/03-notations/12099-master+constraining-terms-occurring-also-as-pattern-in-notations.rst b/doc/changelog/03-notations/12099-master+constraining-terms-occurring-also-as-pattern-in-notations.rst deleted file mode 100644 index e9b02aed6d..0000000000 --- a/doc/changelog/03-notations/12099-master+constraining-terms-occurring-also-as-pattern-in-notations.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - Improved support for notations/abbreviations with mixed terms and patterns (such as the forcing modality) - (`#12099 <https://github.com/coq/coq/pull/12099>`_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12218-numeral-notations-non-inductive.rst b/doc/changelog/03-notations/12218-numeral-notations-non-inductive.rst deleted file mode 100644 index 5ea37e7494..0000000000 --- a/doc/changelog/03-notations/12218-numeral-notations-non-inductive.rst +++ /dev/null @@ -1,19 +0,0 @@ -- **Deprecated** - ``Numeral.v`` is deprecated, please use ``Number.v`` instead. -- **Changed** - Rational and real constants are parsed differently. - The exponent is now encoded separately from the fractional part - using ``Z.pow_pos``. This way, parsing large exponents can no longer - blow up and constants are printed in a form closer to the one they - were parsed (i.e., ``102e-2`` is reprinted as such and not ``1.02``). -- **Removed** - OCaml parser and printer for real constants have been removed. - Real constants are now handled with proven Coq code. -- **Added:** - :ref:`Number Notation <number-notations>` and :ref:`String Notation - <string-notations>` commands now - support parameterized inductive and non inductive types - (`#12218 <https://github.com/coq/coq/pull/12218>`_, - fixes `#12035 <https://github.com/coq/coq/issues/12035>`_, - by Pierre Roux, review by Jason Gross and Jim Fehrle for the - reference manual). diff --git a/doc/changelog/03-notations/12685-master+propagate-scope-in-indirect-applied-ref.rst b/doc/changelog/03-notations/12685-master+propagate-scope-in-indirect-applied-ref.rst deleted file mode 100644 index 048835a0e9..0000000000 --- a/doc/changelog/03-notations/12685-master+propagate-scope-in-indirect-applied-ref.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - Scope information is propagated in indirect applications to a - reference prefixed with :g:`@@`; this covers for instance the case - :g:`r.(@@p) t` where scope information from :g:`p` is now taken into - account for interpreting :g:`t` (`#12685 - <https://github.com/coq/coq/pull/12685>`_, by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12765-master+partial-app-in-recursive-notation.rst b/doc/changelog/03-notations/12765-master+partial-app-in-recursive-notation.rst deleted file mode 100644 index 82cbefc60b..0000000000 --- a/doc/changelog/03-notations/12765-master+partial-app-in-recursive-notation.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Added support for encoding notations of the form :g:`x ⪯ y ⪯ .. ⪯ z ⪯ t` - (`#12765 <https://github.com/coq/coq/pull/12765>`_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12950-master+reorganization-notations-only-parsing-only-printing.rst b/doc/changelog/03-notations/12950-master+reorganization-notations-only-parsing-only-printing.rst deleted file mode 100644 index 16fc91f911..0000000000 --- a/doc/changelog/03-notations/12950-master+reorganization-notations-only-parsing-only-printing.rst +++ /dev/null @@ -1,10 +0,0 @@ -- **Changed:** - New model for ``only parsing`` and ``only printing`` notations with - support for at most one parsing-and-printing or only-parsing - notation per notation and scope, but an arbitrary number of - only-printing notations - (`#12950 <https://github.com/coq/coq/pull/12950>`_, - fixes `#4738 <https://github.com/coq/coq/issues/4738>`_ - and `#9682 <https://github.com/coq/coq/issues/9682>`_ - and part 2 of `#12908 <https://github.com/coq/coq/issues/12908>`_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12960-master+fix9403-missing-flattening-app-notations.rst b/doc/changelog/03-notations/12960-master+fix9403-missing-flattening-app-notations.rst deleted file mode 100644 index fc909e7a1d..0000000000 --- a/doc/changelog/03-notations/12960-master+fix9403-missing-flattening-app-notations.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Fixed:** - Issues in the presence of notations recursively referring to another - applicative notations, such as missing scope propagation, or failure - to use a notation for printing - (`#12960 <https://github.com/coq/coq/pull/12960>`_, - fixes `#9403 <https://github.com/coq/coq/issues/9403>`_ - and `#10803 <https://github.com/coq/coq/issues/10803>`_, - 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 deleted file mode 100644 index e63ab9696e..0000000000 --- a/doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **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/12979-doc-numbers.rst b/doc/changelog/03-notations/12979-doc-numbers.rst deleted file mode 100644 index 631bd6ec69..0000000000 --- a/doc/changelog/03-notations/12979-doc-numbers.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Deprecated:** - :n:`Numeral Notation`, please use :ref:`Number Notation <number-notations>` instead. - (`#12979 <https://github.com/coq/coq/pull/12979>`_, - by Pierre Roux). 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 deleted file mode 100644 index d472e6fdf0..0000000000 --- a/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst +++ /dev/null @@ -1,12 +0,0 @@ -- **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 deleted file mode 100644 index 8b233972bf..0000000000 --- a/doc/changelog/03-notations/12986-master+ordering-notation-by-precision.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **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/03-notations/13092-master+fix-13078-no-binder-in-pattern-notation.rst b/doc/changelog/03-notations/13092-master+fix-13078-no-binder-in-pattern-notation.rst deleted file mode 100644 index fb12c91729..0000000000 --- a/doc/changelog/03-notations/13092-master+fix-13078-no-binder-in-pattern-notation.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Preventing notations for constructors to involve binders - (`#13092 <https://github.com/coq/coq/pull/13092>`_, - fixes `#13078 <https://github.com/coq/coq/issues/13078>`_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/13265-master+allow-single-binder-entry.rst b/doc/changelog/03-notations/13265-master+allow-single-binder-entry.rst deleted file mode 100644 index c973e157dd..0000000000 --- a/doc/changelog/03-notations/13265-master+allow-single-binder-entry.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - The :n:`@binder` entry of :cmd:`Notation` can now be used in - notations expecting a single (non-recursive) binder - (`#13265 <https://github.com/coq/coq/pull/13265>`_, - by Hugo Herbelin, see section :n:`notations-and-binders` of the - reference manual). diff --git a/doc/changelog/03-notations/13415-intern-univs.rst b/doc/changelog/03-notations/13415-intern-univs.rst deleted file mode 100644 index e9f51461e5..0000000000 --- a/doc/changelog/03-notations/13415-intern-univs.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** Notations understand universe names without getting - confused by different imported modules between declaration and use - locations (`#13415 <https://github.com/coq/coq/pull/13415>`_, fixes - `#13303 <https://github.com/coq/coq/issues/13303>`_, by Gaëtan - Gilbert). diff --git a/doc/changelog/03-notations/13519-primitiveArrayNotations.rst b/doc/changelog/03-notations/13519-primitiveArrayNotations.rst new file mode 100644 index 0000000000..fb2545652c --- /dev/null +++ b/doc/changelog/03-notations/13519-primitiveArrayNotations.rst @@ -0,0 +1,8 @@ +- **Added:** + :cmd:`Number Notation` and :cmd:`String Notation` now support + parsing and printing of primitive floats, primitive arrays + and type constants of primitive types. + (`#13519 <https://github.com/coq/coq/pull/13519>`_, + fixes `#13484 <https://github.com/coq/coq/issues/13484>`_ + and `#13517 <https://github.com/coq/coq/issues/13517>`_, + by Fabian Kunze, with help of Jason Gross) diff --git a/doc/changelog/04-tactics/00000-title.rst b/doc/changelog/04-tactics/00000-title.rst index 3c7802d632..afa7821f40 100644 --- a/doc/changelog/04-tactics/00000-title.rst +++ b/doc/changelog/04-tactics/00000-title.rst @@ -1,3 +1,4 @@ -**Tactics** +Tactics +^^^^^^^ diff --git a/doc/changelog/04-tactics/11906-micromega-booleans.rst b/doc/changelog/04-tactics/11906-micromega-booleans.rst deleted file mode 100644 index 39d1525ac3..0000000000 --- a/doc/changelog/04-tactics/11906-micromega-booleans.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - :tacn:`lia` is extended to deal with boolean operators e.g. `andb` or `Z.leb`. - (As `lia` gets more powerful, this may break proof scripts relying on `lia` failure.) - (`#11906 <https://github.com/coq/coq/pull/11906>`_, by Frédéric Besson). diff --git a/doc/changelog/04-tactics/12246-master+apply-in-many-hyps.rst b/doc/changelog/04-tactics/12246-master+apply-in-many-hyps.rst deleted file mode 100644 index 15ab18dcf1..0000000000 --- a/doc/changelog/04-tactics/12246-master+apply-in-many-hyps.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - `apply in` supports several hypotheses - (`#12246 <https://github.com/coq/coq/pull/12246>`_, - by Hugo Herbelin; grants - `#9816 <https://github.com/coq/coq/pull/9816>`_). diff --git a/doc/changelog/04-tactics/12399-rm-prolog.rst b/doc/changelog/04-tactics/12399-rm-prolog.rst deleted file mode 100644 index afde7db370..0000000000 --- a/doc/changelog/04-tactics/12399-rm-prolog.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Removed:** - The deprecated and undocumented "prolog" tactic was removed - (`#12399 <https://github.com/coq/coq/pull/12399>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/04-tactics/12423-rm-info.rst b/doc/changelog/04-tactics/12423-rm-info.rst deleted file mode 100644 index bf20453e6b..0000000000 --- a/doc/changelog/04-tactics/12423-rm-info.rst +++ /dev/null @@ -1,2 +0,0 @@ -- **Removed:** Removed info tactic that was deprecated in 8.5. - (`#12423 <https://github.com/coq/coq/pull/12423>`_, by Jim Fehrle). diff --git a/doc/changelog/04-tactics/12552-zify-pre-hook.rst b/doc/changelog/04-tactics/12552-zify-pre-hook.rst deleted file mode 100644 index 975c917b19..0000000000 --- a/doc/changelog/04-tactics/12552-zify-pre-hook.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Thhe :tacn:`zify` tactic can now be extended by redefining the `zify_pre_hook` - tactic. (`#12552 <https://github.com/coq/coq/pull/12552>`_, - by Kazuhiko Sakaguchi). diff --git a/doc/changelog/04-tactics/12648-zify-int63.rst b/doc/changelog/04-tactics/12648-zify-int63.rst deleted file mode 100644 index ec7a1273e4..0000000000 --- a/doc/changelog/04-tactics/12648-zify-int63.rst +++ /dev/null @@ -1,3 +0,0 @@ -- **Added:** - The :tacn:`zify` tactic provides support for primitive integers (module :g:`ZifyInt63`). - (`#12648 <https://github.com/coq/coq/pull/12648>`_, by Frédéric Besson). 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 deleted file mode 100644 index bc67fd025a..0000000000 --- a/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **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/13337-master+improve-error-dependent-intro-wildcard.rst b/doc/changelog/04-tactics/13337-master+improve-error-dependent-intro-wildcard.rst deleted file mode 100644 index 089647a4b2..0000000000 --- a/doc/changelog/04-tactics/13337-master+improve-error-dependent-intro-wildcard.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Avoiding exposing an internal name of the form :n:`_tmp` when applying the - :n:`_` introduction pattern would break a dependency - (`#13337 <https://github.com/coq/coq/pull/13337>`_, - fixes `#13336 <https://github.com/coq/coq/issues/13336>`_, - by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13373-master+fix13363-metas-posed-to-evars-in-wrong-env.rst b/doc/changelog/04-tactics/13373-master+fix13363-metas-posed-to-evars-in-wrong-env.rst deleted file mode 100644 index c02129a33f..0000000000 --- a/doc/changelog/04-tactics/13373-master+fix13363-metas-posed-to-evars-in-wrong-env.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - The case of tactics, such as :tacn:`eapply`, producing existential variables - under binders with an ill-formed instance - (`#13373 <https://github.com/coq/coq/pull/13373>`_, - fixes `#13363 <https://github.com/coq/coq/issues/13363>`_, - by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13381-bfs_eauto.rst b/doc/changelog/04-tactics/13381-bfs_eauto.rst deleted file mode 100644 index e63241e46c..0000000000 --- a/doc/changelog/04-tactics/13381-bfs_eauto.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Deprecated:** - Undocumented :n:`eauto @nat_or_var @nat_or_var` syntax in favor of new :tacn:`bfs eauto`. - Also deprecated 2-integer syntax for :tacn:`debug eauto` and :tacn:`info_eauto`. - (Use :tacn:`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 deleted file mode 100644 index 5dfa90a267..0000000000 --- a/doc/changelog/04-tactics/13403-occs_nums_nat.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **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/changelog/04-tactics/13417-no_int_or_var.rst b/doc/changelog/04-tactics/13417-no_int_or_var.rst deleted file mode 100644 index 667ee28eea..0000000000 --- a/doc/changelog/04-tactics/13417-no_int_or_var.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Removed:** - A number of tactics that formerly accepted negative - numbers as parameters now give syntax errors for negative - values. These include {e}constructor, do, timeout, - 9 {e}auto tactics and psatz*. - (`#13417 <https://github.com/coq/coq/pull/13417>`_, - by Jim Fehrle). diff --git a/doc/changelog/04-tactics/13469-no-int-in-fail.rst b/doc/changelog/04-tactics/13469-no-int-in-fail.rst new file mode 100644 index 0000000000..e0fcbb924e --- /dev/null +++ b/doc/changelog/04-tactics/13469-no-int-in-fail.rst @@ -0,0 +1,5 @@ +- **Removed:** + :tacn:`fail` and :tacn:`gfail`, which formerly accepted negative + values as a parameter, now give syntax errors for negative + values (`#13469 <https://github.com/coq/coq/pull/13469>`_, + by Jim Fehrle). diff --git a/doc/changelog/04-tactics/13509-master+remove-bracketing-last-introduction-pattern-flag.rst b/doc/changelog/04-tactics/13509-master+remove-bracketing-last-introduction-pattern-flag.rst new file mode 100644 index 0000000000..06c1e280c3 --- /dev/null +++ b/doc/changelog/04-tactics/13509-master+remove-bracketing-last-introduction-pattern-flag.rst @@ -0,0 +1,6 @@ +- **Removed:** + Deprecated flag ``Bracketing Last Introduction Pattern`` affecting the + behavior of trailing disjunctive introduction patterns is + definitively removed + (`#13509 <https://github.com/coq/coq/pull/13509>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst b/doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst new file mode 100644 index 0000000000..aaacb2aadf --- /dev/null +++ b/doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Possible collision between a user-level name and an internal name when + using the :n:`%` introduction pattern + (`#13512 <https://github.com/coq/coq/pull/13512>`_, + fixes `#13413 <https://github.com/coq/coq/issues/13413>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13568-master+fix13566-check-invalid-occurrences-especially-rewrite.rst b/doc/changelog/04-tactics/13568-master+fix13566-check-invalid-occurrences-especially-rewrite.rst new file mode 100644 index 0000000000..160e83f123 --- /dev/null +++ b/doc/changelog/04-tactics/13568-master+fix13566-check-invalid-occurrences-especially-rewrite.rst @@ -0,0 +1,6 @@ +- **Changed:** + More systematic checks that occurrences of an :n:`at` clause are + valid in tactics such as :tacn:`rewrite` or :tacn:`pattern` + (`#13568 <https://github.com/coq/coq/pull/13568>`_, + fixes `#13566 <https://github.com/coq/coq/issues/13566>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13696-deprecate_at_in_conversion.rst b/doc/changelog/04-tactics/13696-deprecate_at_in_conversion.rst new file mode 100644 index 0000000000..306fe8052d --- /dev/null +++ b/doc/changelog/04-tactics/13696-deprecate_at_in_conversion.rst @@ -0,0 +1,7 @@ +- **Deprecated:** + In :tacn:`change` and :tacn:`change_no_check`, the + `at ... with ...` form is deprecated. Use + `with ... at ...` instead. For `at ... with ... in H |-`, + use `with ... in H at ... |-`. + (`#13696 <https://github.com/coq/coq/pull/13696>`_, + by Jim Fehrle). diff --git a/doc/changelog/04-tactics/13699-fix13579.rst b/doc/changelog/04-tactics/13699-fix13579.rst new file mode 100644 index 0000000000..9cf62fb595 --- /dev/null +++ b/doc/changelog/04-tactics/13699-fix13579.rst @@ -0,0 +1,6 @@ +- **Fixed:** + :tacn:`simpl` and :tacn:`hnf` now reduce primitive functions + on primitive integers, floats and arrays + (`#13699 <https://github.com/coq/coq/pull/13699>`_, + fixes `#13579 <https://github.com/coq/coq/issues/13579>`_, + by Pierre Roux). diff --git a/doc/changelog/04-tactics/13715-lia_implb.rst b/doc/changelog/04-tactics/13715-lia_implb.rst new file mode 100644 index 0000000000..dd61872342 --- /dev/null +++ b/doc/changelog/04-tactics/13715-lia_implb.rst @@ -0,0 +1,2 @@ +- **Added:** + :tacn:`lia` supports the boolean operator `Bool.implb` (`#13715 <https://github.com/coq/coq/pull/13715>`_, by Frédéric Besson). diff --git a/doc/changelog/04-tactics/13761-remove_convert_concl_nc.rst b/doc/changelog/04-tactics/13761-remove_convert_concl_nc.rst new file mode 100644 index 0000000000..1aa57ff8b1 --- /dev/null +++ b/doc/changelog/04-tactics/13761-remove_convert_concl_nc.rst @@ -0,0 +1,4 @@ +- **Removed:** + convert_concl_no_check. Use :tacn:`change_no_check` instead + (`#13761 <https://github.com/coq/coq/pull/13761>`_, + by Jim Fehrle). diff --git a/doc/changelog/04-tactics/13762-remove_double_induction.rst b/doc/changelog/04-tactics/13762-remove_double_induction.rst new file mode 100644 index 0000000000..4ea54a1ab6 --- /dev/null +++ b/doc/changelog/04-tactics/13762-remove_double_induction.rst @@ -0,0 +1,9 @@ +- **Removed:** + double induction tactic. Replace :n:`double induction @ident @ident` + with :n:`induction @ident; induction @ident` (or + :n:`induction @ident ; destruct @ident` depending on the exact needs). + Replace :n:`double induction @natural__1 @natural__2` with + :n:`induction @natural__1; induction natural__3` where :n:`natural__3` is the result + of :n:`natural__2 - natural__1` + (`#13762 <https://github.com/coq/coq/pull/13762>`_, + by Jim Fehrle). diff --git a/doc/changelog/04-tactics/13781-deprecate_micromega_options.rst b/doc/changelog/04-tactics/13781-deprecate_micromega_options.rst new file mode 100644 index 0000000000..e3375bd875 --- /dev/null +++ b/doc/changelog/04-tactics/13781-deprecate_micromega_options.rst @@ -0,0 +1,3 @@ +- **Deprecated:** + The micromega option :flag:`Simplex`, which is currently set by default + (`#13781 <https://github.com/coq/coq/pull/13781>`_, by Frédéric Besson). diff --git a/doc/changelog/05-tactic-language/00000-title.rst b/doc/changelog/05-tactic-language/00000-title.rst index b34d190298..bc12b18b7d 100644 --- a/doc/changelog/05-tactic-language/00000-title.rst +++ b/doc/changelog/05-tactic-language/00000-title.rst @@ -1,3 +1,4 @@ -**Tactic language** +Tactic language +^^^^^^^^^^^^^^^ diff --git a/doc/changelog/05-tactic-language/13028-master+fix-quotations-printing.rst b/doc/changelog/05-tactic-language/13028-master+fix-quotations-printing.rst deleted file mode 100644 index a191716b2f..0000000000 --- a/doc/changelog/05-tactic-language/13028-master+fix-quotations-printing.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - printing of the quotation qualifiers when printing :g:`Ltac` functions - (`#13028 <https://github.com/coq/coq/pull/13028>`_, - fixes `#9716 <https://github.com/coq/coq/issues/9716>`_ - and `#13004 <https://github.com/coq/coq/issues/13004>`_, - by Hugo Herbelin). diff --git a/doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst b/doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst deleted file mode 100644 index d105561a23..0000000000 --- a/doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - An if-then-else syntax to Ltac2 - (`#13232 <https://github.com/coq/coq/pull/13232>`_, - fixes `#10110 <https://github.com/coq/coq/issues/10110>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/05-tactic-language/13442-ltac2-abstract-ffi.rst b/doc/changelog/05-tactic-language/13442-ltac2-abstract-ffi.rst new file mode 100644 index 0000000000..26b72de2aa --- /dev/null +++ b/doc/changelog/05-tactic-language/13442-ltac2-abstract-ffi.rst @@ -0,0 +1,6 @@ +- **Added:** + A function Ltac1.lambda allowing to embed Ltac2 functions + into Ltac1 runtime values + (`#13442 <https://github.com/coq/coq/pull/13442>`_, + fixes `#12871 <https://github.com/coq/coq/issues/12871>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/06-ssreflect/00000-title.rst b/doc/changelog/06-ssreflect/00000-title.rst index 2e724627ec..43cccd6d60 100644 --- a/doc/changelog/06-ssreflect/00000-title.rst +++ b/doc/changelog/06-ssreflect/00000-title.rst @@ -1,3 +1,4 @@ -**SSReflect** +SSReflect +^^^^^^^^^ diff --git a/doc/changelog/06-ssreflect/13317-ssr_dup_swap_apply_ipat.rst b/doc/changelog/06-ssreflect/13317-ssr_dup_swap_apply_ipat.rst deleted file mode 100644 index 8d1564533d..0000000000 --- a/doc/changelog/06-ssreflect/13317-ssr_dup_swap_apply_ipat.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - SSReflect intro pattern ltac views ``/[dup]``, ``/[swap]`` and ``/[apply]`` - (`#13317 <https://github.com/coq/coq/pull/13317>`_, - by Cyril Cohen). diff --git a/doc/changelog/06-ssreflect/13459-ssr_dup_swap_apply_ipat.rst b/doc/changelog/06-ssreflect/13459-ssr_dup_swap_apply_ipat.rst deleted file mode 100644 index e14ae89219..0000000000 --- a/doc/changelog/06-ssreflect/13459-ssr_dup_swap_apply_ipat.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - Working around a bug of interaction between + and /(ltac:(...)) cf #13458 - (`#13459 <https://github.com/coq/coq/pull/13459>`_, - by Cyril Cohen). diff --git a/doc/changelog/07-commands-and-options/00000-title.rst b/doc/changelog/07-commands-and-options/00000-title.rst deleted file mode 100644 index 1a0272983e..0000000000 --- a/doc/changelog/07-commands-and-options/00000-title.rst +++ /dev/null @@ -1,3 +0,0 @@ - -**Commands and options** - diff --git a/doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst b/doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst deleted file mode 100644 index 1c7c3102a3..0000000000 --- a/doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Deprecated:** - :cmd:`Grab Existential Variables` and :cmd:`Existential` commands - (`#12516 <https://github.com/coq/coq/pull/12516>`_, - by Maxime Dénès). diff --git a/doc/changelog/07-commands-and-options/13016-remove-Ocaml-value.rst b/doc/changelog/07-commands-and-options/13016-remove-Ocaml-value.rst deleted file mode 100644 index c67b0f6e80..0000000000 --- a/doc/changelog/07-commands-and-options/13016-remove-Ocaml-value.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Removed:** - In the :cmd:`Extraction Language` command, remove `Ocaml` as a valid value. - Use `OCaml` instead. This was deprecated in Coq 8.8, `#6261 <https://github.com/coq/coq/pull/6261>`_ - (`#13016 <https://github.com/coq/coq/pull/13016>`_, by Jim Fehrle). diff --git a/doc/changelog/07-commands-and-options/13040-gc+best_fit.rst b/doc/changelog/07-commands-and-options/13040-gc+best_fit.rst deleted file mode 100644 index 74818f8464..0000000000 --- a/doc/changelog/07-commands-and-options/13040-gc+best_fit.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Changed:** - When compiled with OCaml >= 4.10.0, Coq will use the new best-fit GC - policy, which should provide some performance benefits. Coq's policy - is optimized for speed, but could increase memory consumption in - some cases. You are welcome to tune it using the ``OCAMLRUNPARAM`` - variable and report back setting so we could optimize more. - (`#13040 <https://github.com/coq/coq/pull/13040>`_, - fixes `#11277 <https://github.com/coq/coq/issues/11277>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst b/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst deleted file mode 100644 index 0ab9a58e6f..0000000000 --- a/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - Drop prefixes from grammar non-terminal names, - e.g. "constr:global" -> "global", "Prim.name" -> "name". - Visible in the output of :cmd:`Print Grammar` and :cmd:`Print Custom Grammar`. - (`#13096 <https://github.com/coq/coq/pull/13096>`_, - by Jim Fehrle). diff --git a/doc/changelog/07-commands-and-options/13139-clean-hint-constr.rst b/doc/changelog/07-commands-and-options/13139-clean-hint-constr.rst deleted file mode 100644 index 1a6bc88c6c..0000000000 --- a/doc/changelog/07-commands-and-options/13139-clean-hint-constr.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - When declaring arbitrary terms as hints, unsolved - evars are not abstracted implicitly anymore and instead - raise an error - (`#13139 <https://github.com/coq/coq/pull/13139>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/07-commands-and-options/13255-master+fix13244-use-coercions-in-search.rst b/doc/changelog/07-commands-and-options/13255-master+fix13244-use-coercions-in-search.rst deleted file mode 100644 index 03be92f897..0000000000 --- a/doc/changelog/07-commands-and-options/13255-master+fix13244-use-coercions-in-search.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Added:** - Added support for automatic insertion of coercions in :cmd:`Search` - patterns. Additionally, head patterns are now automatically - interpreted as types - (`#13255 <https://github.com/coq/coq/pull/13255>`_, - fixes `#13244 <https://github.com/coq/coq/issues/13244>`_, - by Hugo Herbelin). diff --git a/doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst b/doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst deleted file mode 100644 index 9ae759be56..0000000000 --- a/doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - The :cmd:`Proof using` command can now be used without loading the - Ltac plugin (`-noinit` mode) - (`#13339 <https://github.com/coq/coq/pull/13339>`_, - by Théo Zimmermann). diff --git a/doc/changelog/07-commands-and-options/13345-master+doc-add-ml-path-not-exported.rst b/doc/changelog/07-commands-and-options/13345-master+doc-add-ml-path-not-exported.rst deleted file mode 100644 index dc8010b456..0000000000 --- a/doc/changelog/07-commands-and-options/13345-master+doc-add-ml-path-not-exported.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Clarify in the documentation that :cmd:`Add ML Path` is not exported to compiled files - (`#13345 <https://github.com/coq/coq/pull/13345>`_, - fixes `#13344 <https://github.com/coq/coq/issues/13344>`_, - by Hugo Herbelin). diff --git a/doc/changelog/07-commands-and-options/13352-cep-48.rst b/doc/changelog/07-commands-and-options/13352-cep-48.rst deleted file mode 100644 index cb2eeea74b..0000000000 --- a/doc/changelog/07-commands-and-options/13352-cep-48.rst +++ /dev/null @@ -1,12 +0,0 @@ -- **Changed:** - Option -native-compiler of the configure script now impacts the - default value of the option -native-compiler of coqc. The - -native-compiler option of the configure script is added an ondemand - value, which becomes the default, thus preserving the previous default - behavior. - The stdlib is still precompiled when configuring with -native-compiler - yes. It is not precompiled otherwise. - This an implementation of point 2 of - `CEP #48 <https://github.com/coq/ceps/pull/48>`_ - (`#13352 <https://github.com/coq/coq/pull/13352>`_, - by Pierre Roux). diff --git a/doc/changelog/07-commands-and-options/13384-warn-unqualified-hint.rst b/doc/changelog/07-commands-and-options/13384-warn-unqualified-hint.rst deleted file mode 100644 index 8ec7198b72..0000000000 --- a/doc/changelog/07-commands-and-options/13384-warn-unqualified-hint.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Deprecated:** - The default value for hint locality is currently :attr:`local` in a section and - :attr:`global` otherwise, but is scheduled to change in a future release. For the - time being, adding hints outside of sections without specifying an explicit - locality is therefore triggering a deprecation warning. It is recommended to - use :attr:`export` whenever possible - (`#13384 <https://github.com/coq/coq/pull/13384>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst b/doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst deleted file mode 100644 index df2bdfeabb..0000000000 --- a/doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - The :attr:`export` locality can now be used for all Hint commands, - including Hint Cut, Hint Mode, Hint Transparent / Opaque and - Remove Hints - (`#13388 <https://github.com/coq/coq/pull/13388>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/07-vernac-commands-and-options/00000-title.rst b/doc/changelog/07-vernac-commands-and-options/00000-title.rst new file mode 100644 index 0000000000..fe50ae0e16 --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/00000-title.rst @@ -0,0 +1,4 @@ + +Commands and options +^^^^^^^^^^^^^^^^^^^^ + diff --git a/doc/changelog/07-vernac-commands-and-options/13725-hint-rw-local.rst b/doc/changelog/07-vernac-commands-and-options/13725-hint-rw-local.rst new file mode 100644 index 0000000000..653e9cd0cd --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/13725-hint-rw-local.rst @@ -0,0 +1,5 @@ +- **Changed:** + :cmd:`Hint Rewrite` now supports locality attributes (including :attr:`export`) like other :ref:`Hint <creating_hints>` commands + (`#13725 <https://github.com/coq/coq/pull/13725>`_, + fixes `#13724 <https://github.com/coq/coq/issues/13724>`_, + by Gaëtan Gilbert). diff --git a/doc/changelog/07-vernac-commands-and-options/13758-remove_hide_obligations.rst b/doc/changelog/07-vernac-commands-and-options/13758-remove_hide_obligations.rst new file mode 100644 index 0000000000..84d6bdea89 --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/13758-remove_hide_obligations.rst @@ -0,0 +1,4 @@ +- **Removed:** + The Hide Obligations flag, deprecated in 8.12 + (`#13758 <https://github.com/coq/coq/pull/13758>`_, + by Jim Fehrle). diff --git a/doc/changelog/07-vernac-commands-and-options/13763-remove_searchhead.rst b/doc/changelog/07-vernac-commands-and-options/13763-remove_searchhead.rst new file mode 100644 index 0000000000..7f0650d8ee --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/13763-remove_searchhead.rst @@ -0,0 +1,4 @@ +- **Removed:** + SearchHead command. Use the `headconcl:` clause of :cmd:`Search` instead + (`#13763 <https://github.com/coq/coq/pull/13763>`_, + by Jim Fehrle). diff --git a/doc/changelog/07-vernac-commands-and-options/13764-remove_add_injtyp.rst b/doc/changelog/07-vernac-commands-and-options/13764-remove_add_injtyp.rst new file mode 100644 index 0000000000..fc6c88eab6 --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/13764-remove_add_injtyp.rst @@ -0,0 +1,6 @@ +- **Removed:** + `Show Zify Spec`, `Add InjTyp` and 11 similar `Add *` commands. + For `Show Zify Spec`, use `Show Zify UnOpSpec` or `Show Zify BinOpSpec` instead. + For `Add *`, `Use Add Zify *` intead of `Add *` + (`#13764 <https://github.com/coq/coq/pull/13764>`_, + by Jim Fehrle). diff --git a/doc/changelog/08-cli-tools/00000-title.rst b/doc/changelog/08-cli-tools/00000-title.rst new file mode 100644 index 0000000000..4c0de43f66 --- /dev/null +++ b/doc/changelog/08-cli-tools/00000-title.rst @@ -0,0 +1,4 @@ + +Command-line tools +^^^^^^^^^^^^^^^^^^ + diff --git a/doc/changelog/08-cli-tools/13822-rm-depr-cmdline.rst b/doc/changelog/08-cli-tools/13822-rm-depr-cmdline.rst new file mode 100644 index 0000000000..e3333f8a9a --- /dev/null +++ b/doc/changelog/08-cli-tools/13822-rm-depr-cmdline.rst @@ -0,0 +1,4 @@ +- **Removed:** previously deprecated command line options + ``-sprop-cumulative`` and ``-input-state`` and its alias ``-is`` + (`#13822 <https://github.com/coq/coq/pull/13822>`_, + by Gaëtan Gilbert). diff --git a/doc/changelog/08-tools/00000-title.rst b/doc/changelog/08-tools/00000-title.rst deleted file mode 100644 index bf462744fb..0000000000 --- a/doc/changelog/08-tools/00000-title.rst +++ /dev/null @@ -1,3 +0,0 @@ - -**Tools** - diff --git a/doc/changelog/08-tools/12389-coq_makefile.rst b/doc/changelog/08-tools/12389-coq_makefile.rst deleted file mode 100644 index 74e3a68170..0000000000 --- a/doc/changelog/08-tools/12389-coq_makefile.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - Adding the possibility in coq_makefile to directly set the installation folders, - through the :n:`COQLIBINSTALL` and :n:`COQDOCINSTALL` variables. - See :ref:`coqmakefilelocal`. - (`#12389 <https://github.com/coq/coq/pull/12389>`_, by Martin Bodin, review of Enrico Tassi). diff --git a/doc/changelog/08-tools/12410-add-fixes.rst b/doc/changelog/08-tools/12410-add-fixes.rst deleted file mode 100644 index f4c41dc3c3..0000000000 --- a/doc/changelog/08-tools/12410-add-fixes.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - ``dev/tools/make-changelog.sh`` now asks for a list of bugs fixed by the PR - (`#12410 <https://github.com/coq/coq/pull/12410>`_, fixes `#12386 - <https://github.com/coq/coq/issues/12386>`_, by Jason Gross). diff --git a/doc/changelog/08-tools/12613-coqchk-noi.rst b/doc/changelog/08-tools/12613-coqchk-noi.rst deleted file mode 100644 index b83c9c69a2..0000000000 --- a/doc/changelog/08-tools/12613-coqchk-noi.rst +++ /dev/null @@ -1,3 +0,0 @@ -- **Removed:** The option ``-I`` of coqchk was removed (it was - deprecated in Coq 8.8) (`#12613 - <https://github.com/coq/coq/pull/12613>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/08-tools/12862-more-mod-checking.rst b/doc/changelog/08-tools/12862-more-mod-checking.rst deleted file mode 100644 index bb1bf9e789..0000000000 --- a/doc/changelog/08-tools/12862-more-mod-checking.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - ``coqchk`` no longer reports names from inner modules of opaque modules as - axioms (`#12862 <https://github.com/coq/coq/pull/12862>`_, fixes `#12845 - <https://github.com/coq/coq/issues/12845>`_, by Jason Gross). diff --git a/doc/changelog/09-coqide/00000-title.rst b/doc/changelog/09-coqide/00000-title.rst index 0fc27cf380..81cf05b844 100644 --- a/doc/changelog/09-coqide/00000-title.rst +++ b/doc/changelog/09-coqide/00000-title.rst @@ -1,3 +1,4 @@ -**CoqIDE** +CoqIDE +^^^^^^ diff --git a/doc/changelog/09-coqide/12874-show_proof_diffs.rst b/doc/changelog/09-coqide/12874-show_proof_diffs.rst deleted file mode 100644 index 51bebad9be..0000000000 --- a/doc/changelog/09-coqide/12874-show_proof_diffs.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Support showing diffs for :cmd:`Show Proof` in CoqIDE from the :n:`View` menu. - See :ref:`showing_proof_diffs`. - (`#12874 <https://github.com/coq/coq/pull/12874>`_, - by Jim Fehrle and Enrico Tassi) diff --git a/doc/changelog/09-coqide/13145-master+coqide-printing-goal-names-support.rst b/doc/changelog/09-coqide/13145-master+coqide-printing-goal-names-support.rst deleted file mode 100644 index f7446cc5aa..0000000000 --- a/doc/changelog/09-coqide/13145-master+coqide-printing-goal-names-support.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Support for flag :flag:`Printing Goal Names` in View menu - (`#13145 <https://github.com/coq/coq/pull/13145>`_, - by Hugo Herbelin). diff --git a/doc/changelog/09-coqide/13810-shift-return-search-backwards.rst b/doc/changelog/09-coqide/13810-shift-return-search-backwards.rst new file mode 100644 index 0000000000..e78280d91d --- /dev/null +++ b/doc/changelog/09-coqide/13810-shift-return-search-backwards.rst @@ -0,0 +1,3 @@ +- **Added:** + Shift-return in the Find dialog now searches backwards (`#13810 <https://github.com/coq/coq/pull/13810>`_, + by slrnsc). diff --git a/doc/changelog/10-standard-library/00000-title.rst b/doc/changelog/10-standard-library/00000-title.rst index d517a0e709..f636f48084 100644 --- a/doc/changelog/10-standard-library/00000-title.rst +++ b/doc/changelog/10-standard-library/00000-title.rst @@ -1,3 +1,4 @@ -**Standard library** +Standard library +^^^^^^^^^^^^^^^^ diff --git a/doc/changelog/10-standard-library/12094-app_inj_tail.rst b/doc/changelog/10-standard-library/12094-app_inj_tail.rst deleted file mode 100644 index 702fbb3d64..0000000000 --- a/doc/changelog/10-standard-library/12094-app_inj_tail.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Extend some list lemmas to both directions: `app_inj_tail_iff`, `app_inv_head_iff`, `app_inv_tail_iff`. - (`#12094 <https://github.com/coq/coq/pull/12094>`_, - fixes `#12093 <https://github.com/coq/coq/issues/12093>`_, - by Edward Wang). diff --git a/doc/changelog/10-standard-library/12186-creal-new-modulus.rst b/doc/changelog/10-standard-library/12186-creal-new-modulus.rst deleted file mode 100644 index 778bf78d59..0000000000 --- a/doc/changelog/10-standard-library/12186-creal-new-modulus.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - In the reals theory changed the epsilon in the definition of the modulus of convergence for CReal from 1/n (n in positive) to 2^z (z in Z) - so that a precision coarser than one is possible. Also added an upper bound to CReal to enable more efficient computations. - (`#12186 <https://github.com/coq/coq/pull/12186>`_, - by Michael Soegtrop). diff --git a/doc/changelog/10-standard-library/12420-decidable.rst b/doc/changelog/10-standard-library/12420-decidable.rst deleted file mode 100644 index 6a4da91fa3..0000000000 --- a/doc/changelog/10-standard-library/12420-decidable.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - ``Decidable`` instance for negation - (`#12420 <https://github.com/coq/coq/pull/12420>`_, - by Yishuai Li). diff --git a/doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst b/doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst deleted file mode 100644 index 208855b4c8..0000000000 --- a/doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Changed:** - Int63 notations now match up with the rest of the standard library: :g:`a \% - m`, :g:`m == n`, :g:`m < n`, :g:`m <= n`, and :g:`m ≤ n` have been replaced - with :g:`a mod m`, :g:`m =? n`, :g:`m <? n`, :g:`m <=? n`, and :g:`m ≤? n`. - The old notations are still available as deprecated notations. Additionally, - there is now a ``Coq.Numbers.Cyclic.Int63.Int63.Int63Notations`` module that - users can import to get the ``Int63`` notations without unqualifying the - various primitives (`#12479 <https://github.com/coq/coq/pull/12479>`_, fixes - `#12454 <https://github.com/coq/coq/issues/12454>`_, by Jason Gross). diff --git a/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst b/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst deleted file mode 100644 index 1709cf1eae..0000000000 --- a/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Changed:** - PrimFloat notations now match up with the rest of the standard library: :g:`m - == n`, :g:`m < n`, and :g:`m <= n` have been replaced with :g:`m =? n`, :g:`m - <? n`, and :g:`m <=? n`. The old notations are still available as deprecated - notations. Additionally, there is now a - ``Coq.Floats.PrimFloat.PrimFloatNotations`` module that users can import to - get the ``PrimFloat`` notations without unqualifying the various primitives - (`#12556 <https://github.com/coq/coq/pull/12556>`_, fixes `#12454 - <https://github.com/coq/coq/issues/12454>`_, by Jason Gross). diff --git a/doc/changelog/10-standard-library/12716-curry.rst b/doc/changelog/10-standard-library/12716-curry.rst deleted file mode 100644 index 51b59e4a94..0000000000 --- a/doc/changelog/10-standard-library/12716-curry.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Deprecated:** - ``prod_curry`` and ``prod_uncurry``, in favor of ``uncurry`` and ``curry`` - (`#12716 <https://github.com/coq/coq/pull/12716>`_, - by Yishuai Li). diff --git a/doc/changelog/10-standard-library/12799-list-repeat.rst b/doc/changelog/10-standard-library/12799-list-repeat.rst deleted file mode 100644 index adfc48f67b..0000000000 --- a/doc/changelog/10-standard-library/12799-list-repeat.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - New lemmas about ``repeat`` in ``List`` and ``Permutation``: ``repeat_app``, ``repeat_eq_app``, ``repeat_eq_cons``, ``repeat_eq_elt``, ``Forall_eq_repeat``, ``Permutation_repeat`` - (`#12799 <https://github.com/coq/coq/pull/12799>`_, - by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12801-cyclic-set.rst b/doc/changelog/10-standard-library/12801-cyclic-set.rst deleted file mode 100644 index 9a07d78144..0000000000 --- a/doc/changelog/10-standard-library/12801-cyclic-set.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - Change the sort of cyclic numbers from Type to Set. For backward compatibility, a dynamic sort was defined in the 3 packages bignums, coqprime and color. - See for example commit 6f62bda in bignums. - (`#12801 <https://github.com/coq/coq/pull/12801>`_, - by Vincent Semeria). diff --git a/doc/changelog/10-standard-library/12861-nsatz-tactic-instances.rst b/doc/changelog/10-standard-library/12861-nsatz-tactic-instances.rst deleted file mode 100644 index 41359098e3..0000000000 --- a/doc/changelog/10-standard-library/12861-nsatz-tactic-instances.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Changed:** - ``Require Import Coq.nsatz.NsatzTactic`` now allows using :tacn:`nsatz` - with `Z` and `Q` without having to supply instances or using ``Require Import Coq.nsatz.Nsatz``, which - transitively requires unneeded files declaring axioms used in the reals - (`#12861 <https://github.com/coq/coq/pull/12861>`_, - fixes `#12860 <https://github.com/coq/coq/issues/12860>`_, - by Jason Gross). diff --git a/doc/changelog/10-standard-library/13365-axiom-free-wf.rst b/doc/changelog/10-standard-library/13365-axiom-free-wf.rst deleted file mode 100644 index 1fc40894eb..0000000000 --- a/doc/changelog/10-standard-library/13365-axiom-free-wf.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - `Coq.Program.Wf.Fix_F_inv` and `Coq.Program.Wf.Fix_eq` are now axiom-free. They no longer assume proof irrelevance. - (`#13365 <https://github.com/coq/coq/pull/13365>`_, - by Li-yao Xia). diff --git a/doc/changelog/10-standard-library/13582-exp_ineq.rst b/doc/changelog/10-standard-library/13582-exp_ineq.rst new file mode 100644 index 0000000000..27d89b2f8b --- /dev/null +++ b/doc/changelog/10-standard-library/13582-exp_ineq.rst @@ -0,0 +1,9 @@ +- **Changed:** + Minor Changes to Rpower: + Generalizes exp_ineq1 to hold for all non-zero numbers. + Adds exp_ineq1_le, which holds for all reals (but is a <= instead of a <). + + (`#13582 <https://github.com/coq/coq/pull/13582>`_, + by Avi Shinnar and Barry Trager, with help from Laurent Théry + +). diff --git a/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst b/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst index 6b301f59d3..7358fe192f 100644 --- a/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst +++ b/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst @@ -1,3 +1,4 @@ -**Infrastructure and dependencies** +Infrastructure and dependencies +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/doc/changelog/11-infrastructure-and-dependencies/11742-zarith+core.rst b/doc/changelog/11-infrastructure-and-dependencies/11742-zarith+core.rst deleted file mode 100644 index 3b34e11ff8..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/11742-zarith+core.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Changed:** - Coq's core system now uses the `zarith <https://github.com/ocaml/Zarith>`_ - library, based on GNU's gmp instead of ``num`` which is - deprecated upstream. The custom ``bigint`` module is - not longer provided; note that the ``micromega`` still uses - ``num`` - (`#11742 <https://github.com/coq/coq/pull/11742>`_, - by Emilio Jesus Gallego Arias and Vicent Laporte). diff --git a/doc/changelog/11-infrastructure-and-dependencies/13007-zarith+goodbye_num.rst b/doc/changelog/11-infrastructure-and-dependencies/13007-zarith+goodbye_num.rst deleted file mode 100644 index c142eec561..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/13007-zarith+goodbye_num.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Removed:** - The `num` library is not linked to Coq anymore - (`#13007 <https://github.com/coq/coq/pull/13007>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/12-misc/00000-title.rst b/doc/changelog/12-misc/00000-title.rst index 5e709e2b27..1391ec2164 100644 --- a/doc/changelog/12-misc/00000-title.rst +++ b/doc/changelog/12-misc/00000-title.rst @@ -1,3 +1,4 @@ -**Miscellaneous** +Miscellaneous +^^^^^^^^^^^^^ diff --git a/doc/changelog/12-misc/12586-declare+typing_flags.rst b/doc/changelog/12-misc/12586-declare+typing_flags.rst deleted file mode 100644 index 52915ceee9..0000000000 --- a/doc/changelog/12-misc/12586-declare+typing_flags.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - Typing flags can now be specified per-constant / inductive, this - allows to fine-grain specify them from plugins or attributes. See - :ref:`controlling-typing-flags` for details on attribute syntax. - (`#12586 <https://github.com/coq/coq/pull/12586>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index bfdbc4c4db..9495fd0e45 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -107,7 +107,7 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica .. cmd:: Axiom @ident : @term. This command links :token:`term` to the name :token:`term` as its specification in - the global context. The fact asserted by :token:`term` is thus assumed as a + the global environment. The fact asserted by :token:`term` is thus assumed as a postulate. .. cmdv:: Parameter @ident : @term. diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 3662822a5e..8e72bb4ffd 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -100,7 +100,6 @@ Setting the target language ~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Extraction Language @language - :name: Extraction Language .. insertprodn language language @@ -431,12 +430,10 @@ Additional settings ~~~~~~~~~~~~~~~~~~~ .. opt:: Extraction File Comment @string - :name: Extraction File Comment Provides a comment that is included at the beginning of the output files. .. opt:: Extraction Flag @natural - :name: Extraction Flag Controls which optimizations are used during extraction, providing a finer-grained control than :flag:`Extraction Optimize`. The bits of :token:`natural` are used as a bit mask. diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 039a23e8c2..9ac05fab2e 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -101,7 +101,7 @@ morphisms, that are required to be simultaneously monotone on every argument. Morphisms can also be contravariant in one or more of their arguments. -A morphism is contravariant on an argument associated to the relation +A morphism is contravariant on an argument associated with the relation instance :math:`R` if it is covariant on the same argument when the inverse relation :math:`R^{−1}` (``inverse R`` in Coq) is considered. The special arrow ``-->`` is used in signatures for contravariant morphisms. @@ -336,7 +336,7 @@ respective relation instances. in the previous example). Applying ``union_compat`` by hand we are left with the goal ``eq_set (union S S) (union S S)``. -When the relations associated to some arguments are not reflexive, the +When the relations associated with some arguments are not reflexive, the tactic cannot automatically prove the reflexivity goals, that are left to the user. @@ -477,8 +477,8 @@ documentation on :ref:`typeclasses` and the theories files in Classes for further explanations. One can inform the rewrite tactic about morphisms and relations just -by using the typeclass mechanism to declare them using Instance and -Context vernacular commands. Any object of type Proper (the type of +by using the typeclass mechanism to declare them using the :cmd:`Instance` and +:cmd:`Context` commands. Any object of type Proper (the type of morphism declarations) in the local context will also be automatically used by the rewriting tactic to solve constraints. @@ -553,7 +553,7 @@ pass additional arguments such as ``using relation``. be used to replace the first tactic argument with the second one. If omitted, it defaults to the ``DefaultRelation`` instance on the type of the objects. By default, it means the most recent ``Equivalence`` instance - in the environment, but it can be customized by declaring + in the global environment, but it can be customized by declaring new ``DefaultRelation`` instances. As Leibniz equality is a declared equivalence, it will fall back to it if no other relation is declared on a given type. @@ -608,7 +608,6 @@ Deprecated syntax and backward incompatibilities an old development to the new semantics is usually quite simple. .. cmd:: Declare Morphism @one_term : @ident - :name: Declare Morphism Declares a parameter in a module type that is a morphism. @@ -686,7 +685,7 @@ Note that when one does rewriting with a lemma under a binder using variable, as the semantics are different from rewrite where the lemma is first matched on the whole term. With the new :tacn:`setoid_rewrite`, matching is done on each subterm separately and in its local -environment, and all matches are rewritten *simultaneously* by +context, and all matches are rewritten *simultaneously* by default. The semantics of the previous :tacn:`setoid_rewrite` implementation can almost be recovered using the ``at 1`` modifier. @@ -727,6 +726,30 @@ declare your constant as rigid for proof search using the command Strategies for rewriting ------------------------ +Usage +~~~~~ + +.. tacn:: rewrite_strat @rewstrategy {? in @ident } + :name: rewrite_strat + + Rewrite using :n:`@rewstrategy` in the conclusion or in the hypothesis :n:`@ident`. + + .. exn:: Nothing to rewrite. + + The strategy didn't find any matches. + + .. exn:: No progress made. + + If the strategy succeeded but made no progress. + + .. exn:: Unable to satisfy the rewriting constraints. + + If the strategy succeeded and made progress but the + corresponding rewriting constraints are not satisfied. + + :tacn:`setoid_rewrite` :n:`@one_term` is basically equivalent to + :n:`rewrite_strat outermost @one_term`. + Definitions ~~~~~~~~~~~ @@ -774,7 +797,7 @@ are applied using the tactic :n:`rewrite_strat @rewstrategy`. failure :n:`id` - identity + identity :n:`refl` reflexivity @@ -804,10 +827,16 @@ are applied using the tactic :n:`rewrite_strat @rewstrategy`. all subterms :n:`innermost @rewstrategy` - innermost first + Innermost first. + When there are multiple nested matches in a subterm, the innermost subterm + is rewritten. For :ref:`example <rewrite_strat_innermost_outermost>`, + rewriting :n:`(a + b) + c` with Nat.add_comm gives :n:`(b + a) + c`. :n:`outermost @rewstrategy` - outermost first + Outermost first. + When there are multiple nested matches in a subterm, the outermost subterm + is rewritten. For :ref:`example <rewrite_strat_innermost_outermost>`, + rewriting :n:`(a + b) + c` with Nat.add_comm gives :n:`c + (a + b)`. :n:`bottomup @rewstrategy` bottom-up @@ -834,8 +863,8 @@ are applied using the tactic :n:`rewrite_strat @rewstrategy`. to be documented -A few of these are defined in terms of the others using a -primitive fixpoint operator: +Conceptually, a few of these are defined in terms of the others using a +primitive fixpoint operator `fix`, which the tactic doesn't currently support: - :n:`try @rewstrategy := choice @rewstrategy id` - :n:`any @rewstrategy := fix @ident. try (@rewstrategy ; @ident)` @@ -877,30 +906,30 @@ if it reduces the subterm under consideration. The ``fold`` strategy takes a :token:`term` and tries to *unify* it to the current subterm, converting it to :token:`term` on success. It is stronger than the tactic ``fold``. +.. _rewrite_strat_innermost_outermost: -Usage -~~~~~ - - -.. tacn:: rewrite_strat @rewstrategy {? in @ident } - :name: rewrite_strat +.. example:: :n:`innermost` and :n:`outermost` - Rewrite using the strategy s in hypothesis ident or the conclusion. + The type of `Nat.add_comm` is `forall n m : nat, n + m = m + n`. - .. exn:: Nothing to rewrite. + .. coqtop:: all - If the strategy failed. + Require Import Coq.Arith.Arith. + Set Printing Parentheses. + Goal forall a b c: nat, a + b + c = 0. + rewrite_strat innermost Nat.add_comm. - .. exn:: No progress made. + .. coqtop:: none - If the strategy succeeded but made no progress. + Abort. + Goal forall a b c: nat, a + b + c = 0. - .. exn:: Unable to satisfy the rewriting constraints. + Using :n:`outermost` instead gives this result: - If the strategy succeeded and made progress but the - corresponding rewriting constraints are not satisfied. + .. coqtop:: all + rewrite_strat outermost Nat.add_comm. - The ``setoid_rewrite c`` tactic is basically equivalent to - ``rewrite_strat (outermost c)``. + .. coqtop:: none + Abort. diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 0f0ccd6a20..09b2bb003a 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -202,7 +202,6 @@ Use :n:`:>` instead of :n:`:` before the :undocumented: .. cmd:: SubClass @ident_decl @def_body - :name: SubClass If :n:`@type` is a class :n:`@ident'` applied to some arguments then :n:`@ident` is defined and an identity coercion of name @@ -243,7 +242,6 @@ Activating the Printing of Coercions By default, coercions are not printed. .. table:: Printing Coercion @qualid - :name: Printing Coercion Specifies a set of qualids for which coercions are always displayed. Use the :cmd:`Add` and :cmd:`Remove` commands to update the set of qualids. diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 28b60878d2..5d471c695c 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -31,9 +31,11 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`, .. flag:: Simplex + .. deprecated:: 8.14 + This flag (set by default) instructs the decision procedures to - use the Simplex method for solving linear goals. If it is not set, - the decision procedures are using Fourier elimination. + use the Simplex method for solving linear goals instead of the + deprecated Fourier elimination. .. opt:: Dump Arith @@ -140,7 +142,6 @@ and checked to be :math:`-1`. ------------------------------------------------------------------- .. tacn:: lra - :name: lra This tactic is searching for *linear* refutations. As a result, this tactic explores a subset of the *Cone* defined as @@ -154,7 +155,6 @@ and checked to be :math:`-1`. --------------------------------------------- .. tacn:: lia - :name: lia This tactic solves linear goals over :g:`Z` by searching for *linear* refutations and cutting planes. :tacn:`lia` provides support for :g:`Z`, :g:`nat`, :g:`positive` and :g:`N` by pre-processing via the :tacn:`zify` tactic. @@ -220,7 +220,6 @@ a proof. -------------------------------------------------- .. tacn:: nra - :name: nra This tactic is an *experimental* proof procedure for non-linear arithmetic. The tactic performs a limited amount of non-linear @@ -241,7 +240,6 @@ proof by abstracting monomials by variables. ---------------------------------------------------------- .. tacn:: nia - :name: nia This tactic is a proof procedure for non-linear integer arithmetic. It performs a pre-processing similar to :tacn:`nra`. The obtained goal is @@ -251,7 +249,6 @@ proof by abstracting monomials by variables. ---------------------------------------------------- .. tacn:: psatz @one_term {? @nat_or_var } - :name: psatz This tactic explores the *Cone* by increasing degrees – hence the depth parameter :token:`nat_or_var`. In theory, such a proof search is complete – if the @@ -281,7 +278,6 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. ------------------------------------------ .. tacn:: zify - :name: zify This tactic is internally called by :tacn:`lia` to support additional types, e.g., :g:`nat`, :g:`positive` and :g:`N`. Additional support is provided by the following modules: @@ -321,68 +317,6 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. prints the list of types that supported by :tacn:`zify` i.e., :g:`Z`, :g:`nat`, :g:`positive` and :g:`N`. -.. cmd:: Show Zify Spec - - .. deprecated:: 8.13 - Use :cmd:`Show Zify` ``UnOpSpec`` or :cmd:`Show Zify` ``BinOpSpec`` instead. - -.. cmd:: Add InjTyp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``InjTyp`` instead. - -.. cmd:: Add BinOp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``BinOp`` instead. - -.. cmd:: Add BinOpSpec @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``BinOpSpec`` instead. - -.. cmd:: Add UnOp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``UnOp`` instead. - -.. cmd:: Add UnOpSpec @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``UnOpSpec`` instead. - -.. cmd:: Add CstOp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``CstOp`` instead. - -.. cmd:: Add BinRel @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``BinRel`` instead. - -.. cmd:: Add PropOp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``PropOp`` instead. - -.. cmd:: Add PropBinOp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``PropBinOp`` instead. - -.. cmd:: Add PropUOp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``PropUOp`` instead. - -.. cmd:: Add Saturate @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``Saturate`` instead. - - - .. [#csdp] Sources and binaries can be found at https://projects.coin-or.org/Csdp .. [#fnpsatz] Variants deal with equalities and strict inequalities. diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 2b10f5671d..0997c5e868 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -28,7 +28,6 @@ Description of ``omega`` ------------------------ .. tacn:: omega - :name: omega .. deprecated:: 8.12 diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index e824ae152d..ea506cec84 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -70,7 +70,7 @@ Coq 8.6 introduced a mechanism for error resilience: in interactive mode Coq is able to completely check a document containing errors instead of bailing out at the first failure. -Two kind of errors are supported: errors occurring in vernacular +Two kind of errors are supported: errors occurring in commands and errors occurring in proofs. To properly recover from a failing tactic, Coq needs to recognize the @@ -89,8 +89,8 @@ kind of proof blocks, and an ML API to add new ones. Caveats ```````` -When a vernacular command fails the subsequent error messages may be -bogus, i.e. caused by the first error. Error resilience for vernacular +When a command fails the subsequent error messages may be +bogus, i.e. caused by the first error. Error resilience for commands can be switched off by passing ``-async-proofs-command-error-resilience off`` to CoqIDE. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 104f84a253..8f2b51ccce 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -161,7 +161,7 @@ Program Definition A :cmd:`Definition` command with the :attr:`program` attribute types the value term in Russell and generates proof obligations. Once solved using the commands shown below, it binds the -final Coq term to the name :n:`@ident` in the environment. +final Coq term to the name :n:`@ident` in the global environment. :n:`Program Definition @ident : @type := @term` @@ -268,7 +268,6 @@ obligations (e.g. when defining mutually recursive blocks). The optional tactic is replaced by the default one if not specified. .. cmd:: Obligation Tactic := @ltac_expr - :name: Obligation Tactic Sets the default obligation solving tactic applied to all obligations automatically, whether to solve them or when starting to prove one, @@ -321,14 +320,6 @@ optional tactic is replaced by the default one if not specified. (the default), or if the system should infer which obligations can be declared opaque. -.. flag:: Hide Obligations - - .. deprecated:: 8.12 - - Controls whether obligations appearing in the - term should be hidden as implicit arguments of the special - constant ``Program.Tactics.obligation``. - The module :g:`Coq.Program.Tactics` defines the default tactic for solving obligations called :g:`program_simpl`. Importing :g:`Coq.Program.Program` also adds some useful notations, as documented in the file itself. diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index c93d621048..954c2c1446 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -421,7 +421,7 @@ Error messages: .. exn:: Ring operation should be declared as a morphism. - A setoid associated to the carrier of the ring structure has been found, + A setoid associated with the carrier of the ring structure has been found, but the ring operation should be declared as morphism. See :ref:`tactics-enabled-on-user-provided-relations`. How does it work? diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst index 2b1f343e14..8c20e08154 100644 --- a/doc/sphinx/addendum/sprop.rst +++ b/doc/sphinx/addendum/sprop.rst @@ -19,7 +19,6 @@ Use of |SProp| may be disabled by passing ``-disallow-sprop`` to the Coq program or by turning the :flag:`Allow StrictProp` flag off. .. flag:: Allow StrictProp - :name: Allow StrictProp Enables or disables the use of |SProp|. It is enabled by default. The command-line flag ``-disallow-sprop`` disables |SProp| at @@ -283,7 +282,6 @@ This means that some errors will be delayed until ``Qed``: Abort. .. flag:: Elaboration StrictProp Cumulativity - :name: Elaboration StrictProp Cumulativity Unset this flag (it is on by default) to be strict with regard to :math:`\SProp` cumulativity during elaboration. @@ -320,7 +318,6 @@ so correctly converts ``x`` and ``y``. it to find when your tactics are producing incorrect marks. .. flag:: Cumulative StrictProp - :name: Cumulative StrictProp Set this flag (it is off by default) to make the kernel accept cumulativity between |SProp| and other universes. This makes diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 4143d836c4..8dc0030115 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -160,7 +160,7 @@ Sections and contexts --------------------- To ease developments parameterized by many instances, one can use the -:cmd:`Context` command to introduce these parameters into section contexts, +:cmd:`Context` command to introduce the parameters into the :term:`local context`, it works similarly to the command :cmd:`Variable`, except it accepts any binding context as an argument, so variables can be implicit, and :ref:`implicit-generalization` can be used. @@ -422,7 +422,7 @@ Summary of the commands resolution with the local hypotheses use full conversion during unification. - + The mode hints (see :cmd:`Hint Mode`) associated to a class are + + The mode hints (see :cmd:`Hint Mode`) associated with a class are taken into account by :tacn:`typeclasses eauto`. When a goal does not match any of the declared modes for its head (if any), instead of failing like :tacn:`eauto`, the goal is suspended and @@ -470,7 +470,6 @@ Summary of the commands refinement engine will be able to backtrack. .. tacn:: autoapply @one_term with @ident - :name: autoapply The tactic ``autoapply`` applies :token:`one_term` using the transparency information of the hint database :token:`ident`, and does *no* typeclass resolution. This can @@ -590,7 +589,6 @@ Settings :cmd:`Typeclasses eauto` is another way to set this flag. .. opt:: Typeclasses Depth @natural - :name: Typeclasses Depth Sets the maximum proof search depth. The default is unbounded. :cmd:`Typeclasses eauto` is another way to set this option. @@ -602,7 +600,6 @@ Settings is another way to set this flag. .. opt:: Typeclasses Debug Verbosity @natural - :name: Typeclasses Debug Verbosity Determines how much information is shown for typeclass resolution steps during search. 1 is the default level. 2 shows additional information such as tried tactics and shelving @@ -613,7 +610,6 @@ Typeclasses eauto ~~~~~~~~~~~~~~~~~ .. cmd:: Typeclasses eauto := {? debug } {? ( {| bfs | dfs } ) } {? @natural } - :name: Typeclasses eauto Allows more global customization of the :tacn:`typeclasses eauto` tactic. The options are: diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index bb78b142ca..d0b05a03f9 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -328,7 +328,7 @@ Cumulativity Weak Constraints Global and local universes --------------------------- -Each universe is declared in a global or local environment before it +Each universe is declared in a global or local context before it can be used. To ensure compatibility, every *global* universe is set to be strictly greater than :g:`Set` when it is introduced, while every *local* (i.e. polymorphically quantified) universe is introduced as @@ -617,7 +617,7 @@ definitions in the section sharing a common variable will both get parameterized by the universes produced by the variable declaration. This is in contrast to a “mononorphic” variable which introduces global universes and constraints, making the two definitions depend on -the *same* global universes associated to the variable. +the *same* global universes associated with the variable. It is possible to mix universe polymorphism and monomorphism in sections, except in the following ways: diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 249c7794be..ea099eb52e 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -8,6 +8,720 @@ Recent changes .. include:: ../unreleased.rst +Version 8.13 +------------ + +Summary of changes +~~~~~~~~~~~~~~~~~~ + +Coq version 8.13 integrates many usability improvements, as well +as extensions of the core language. +The main changes include: + + - :ref:`Introduction <813PrimArrays>` of :ref:`primitive persistent arrays<primitive-arrays>` + in the core language, implemented using imperative persistent arrays. + - Introduction of :ref:`definitional proof irrelevance <813UIP>` for the equality type + defined in the SProp sort. + - Cumulative record and inductive type declarations can now + :ref:`specify <813VarianceDecl>` the variance of their universes. + - Various bugfixes and uniformization of behavior with respect to the use of + implicit arguments and the handling of existential variables in + declarations, unification and tactics. + - New warning for :ref:`unused variables <813UnusedVar>` in catch-all match + branches that match multiple distinct patterns. + - New :ref:`warning <813HintWarning>` for `Hint` commands outside + sections without a locality attribute, whose goal is to eventually + remove the fragile default behavior of importing hints only when + using `Require`. The recommended fix is to declare hints as `export`, + instead of the current default `global`, meaning that they are imported + through `Require Import` only, not `Require`. + See the following `rationale and guidelines <https://coq.discourse.group/t/change-of-default-locality-for-hint-commands-in-coq-8-13/1140>`_ + for details. + - General support for :ref:`boolean attributes <813BooleanAttrs>`. + - Many improvements to the handling of :ref:`notations <813Notations>`, + including number notations, recursive notations and notations with bindings. + A new algorithm chooses the most precise notation available to print an expression, + which might introduce changes in printing behavior. + - Tactic :ref:`improvements <813Tactics>` in :tacn:`lia` and its :tacn:`zify` preprocessing step, + now supporting reasoning on boolean operators such as :g:`Z.leb` and supporting + primitive integers :g:`Int63`. + - Typing flags can now be specified :ref:`per-constant / inductive <813TypingFlags>`. + - Improvements to the reference manual including updated syntax + descriptions that match Coq's grammar in several chapters, and splitting parts of + the tactics chapter to independent sections. + +See the `Changes in 8.13+beta1`_ section and following sections for the +detailed list of changes, including potentially breaking changes marked +with **Changed**. + +Coq's documentation is available at https://coq.github.io/doc/v8.13/refman (reference +manual), and https://coq.github.io/doc/v8.13/stdlib (documentation of +the standard library). Developer documentation of the ML API is available +at https://coq.github.io/doc/v8.13/api. + +Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael +Soegtrop and Théo Zimmermann worked on maintaining and improving the +continuous integration system and package building infrastructure. + +Erik Martin-Dorel has maintained the `Coq Docker images +<https://hub.docker.com/r/coqorg/coq>`_ that are used in many Coq +projects for continuous integration. + +The OPAM repository for Coq packages has been maintained by +Guillaume Claret, Karl Palmskog, Matthieu Sozeau and Enrico Tassi with +contributions from many users. A list of packages is available at +https://coq.inria.fr/opam/www/. + +Our current 32 maintainers are Yves Bertot, Frédéric Besson, Tej +Chajed, Cyril Cohen, Pierre Corbineau, Pierre Courtieu, Maxime Dénès, +Jim Fehrle, Julien Forest, Emilio Jesús Gallego Arias, Gaëtan Gilbert, +Georges Gonthier, Benjamin Grégoire, Jason Gross, Hugo Herbelin, +Vincent Laporte, Olivier Laurent, Assia Mahboubi, Kenji Maillard, +Guillaume Melquiond, Pierre-Marie Pédrot, Clément Pit-Claudel, +Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Arnaud Spiwack, +Matthieu Sozeau, Enrico Tassi, Laurent Théry, Anton Trunov, Li-yao Xia +and Théo Zimmermann. + +The 52 contributors to this version are Reynald Affeldt, Tanaka Akira, Frédéric +Besson, Lasse Blaauwbroek, Clément Blaudeau, Martin Bodin, Ali Caglayan, Tej Chajed, +Cyril Cohen, Julien Coolen, Matthew Dempsky, Maxime Dénès, Andres Erbsen, +Jim Fehrle, Emilio Jesús Gallego Arias, Paolo G. Giarrusso, Attila Gáspár, Gaëtan Gilbert, +Jason Gross, Benjamin Grégoire, Hugo Herbelin, Wolf Honore, Jasper Hugunin, Ignat Insarov, +Ralf Jung, Fabian Kunze, Vincent Laporte, Olivier Laurent, Larry D. Lee Jr, +Thomas Letan, Yishuai Li, Xia Li-yao, James Lottes, Jean-Christophe Léchenet, +Kenji Maillard, Erik Martin-Dorel, Yusuke Matsushita, Guillaume Melquiond, +Carl Patenaude-Poulin, Clément Pit-Claudel, Pierre-Marie Pédrot, Pierre Roux, +Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Matthieu Sozeau, +Enrico Tassi, Anton Trunov, Edward Wang, Li-yao Xia, Beta Ziliani and Théo Zimmermann. + +The Coq community at large helped improve the design of this new version via +the GitHub issue and pull request system, the Coq development mailing list +coqdev@inria.fr, the coq-club@inria.fr mailing list, the `Discourse forum +<https://coq.discourse.group/>`_ and the `Coq Zulip chat <http://coq.zulipchat.com>`_. + +Version 8.13's development spanned 5 months from the release of +Coq 8.12.0. Enrico Tassi and Maxime Dénès are the release managers of Coq 8.13. +This release is the result of 400 merged PRs, closing ~100 issues. + +| Nantes, November 2020, +| Matthieu Sozeau for the Coq development team +| + + +Changes in 8.13+beta1 +~~~~~~~~~~~~~~~~~~~~~ + +.. contents:: + :local: + +Kernel +^^^^^^ + + .. _813UIP: + +- **Added:** + Definitional UIP, only when :flag:`Definitional UIP` is enabled. + This models definitional uniqueness of identity proofs for the equality + type in SProp. It is deactivated by default as it can lead to + non-termination in combination with impredicativity. + Use of this flag is also printed by :cmd:`Print Assumptions`. See + documentation of the flag for details. + (`#10390 <https://github.com/coq/coq/pull/10390>`_, + by Gaëtan Gilbert). + + .. _813PrimArrays: + +- **Added:** + Built-in support for persistent arrays, which expose a functional + interface but are implemented using an imperative data structure, for + better performance. + (`#11604 <https://github.com/coq/coq/pull/11604>`_, + by Maxime Dénès and Benjamin Grégoire, with help from Gaëtan Gilbert). + + Primitive arrays are irrelevant in their single + polymorphic universe (same as a polymorphic cumulative list + inductive would be) (`#13356 + <https://github.com/coq/coq/pull/13356>`_, fixes `#13354 + <https://github.com/coq/coq/issues/13354>`_, by Gaëtan Gilbert). + +- **Fixed:** + A loss of definitional equality for declarations obtained through + :cmd:`Include` when entering the scope of a :cmd:`Module` or + :cmd:`Module Type` was causing :cmd:`Search` not to see the included + declarations + (`#12537 <https://github.com/coq/coq/pull/12537>`_, fixes `#12525 + <https://github.com/coq/coq/pull/12525>`_ and `#12647 + <https://github.com/coq/coq/pull/12647>`_, by Hugo Herbelin). + +- **Fixed:** + Fix an incompleteness in the typechecking of `match` for + cumulative inductive types. This could result in breaking subject + reduction. + (`#13501 <https://github.com/coq/coq/pull/13501>`_, + fixes `#13495 <https://github.com/coq/coq/issues/13495>`_, + by Matthieu Sozeau). + +Specification language, type inference +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + + .. _813BooleanAttrs: + +- **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). +- **Changed:** Heuristics for universe minimization to :g:`Set`: also + use constraints ``Prop <= i`` (`#10331 + <https://github.com/coq/coq/pull/10331>`_, by Gaëtan Gilbert with + help from Maxime Dénès and Matthieu Sozeau, fixes `#12414 + <https://github.com/coq/coq/issues/12414>`_). +- **Changed:** The type given to :cmd:`Instance` is no longer automatically + generalized over unbound and :ref:`generalizable <implicit-generalization>` variables. + Use ``Instance : `{type}`` instead of :n:`Instance : @type` to get the old behaviour, or + enable the compatibility flag :flag:`Instance Generalized Output`. + (`#13188 <https://github.com/coq/coq/pull/13188>`_, fixes `#6042 + <https://github.com/coq/coq/issues/6042>`_, by Gaëtan Gilbert). +- **Changed:** + Tweaked the algorithm giving default names to arguments. + Should reduce the frequency that argument names get an + unexpected suffix. + Also makes :flag:`Mangle Names` not mess up argument names. + (`#12756 <https://github.com/coq/coq/pull/12756>`_, + fixes `#12001 <https://github.com/coq/coq/issues/12001>`_ + and `#6785 <https://github.com/coq/coq/issues/6785>`_, + by Jasper Hugunin). +- **Removed:** + Undocumented and experimental forward class hint feature ``:>>``. + Use ``:>`` (see :n:`@of_type`) instead + (`#13106 <https://github.com/coq/coq/pull/13106>`_, + by Pierre-Marie Pédrot). + + .. _813VarianceDecl: + +- **Added:** Commands :cmd:`Inductive`, :cmd:`Record` and synonyms now + support syntax `Inductive foo@{=i +j *k l}` to specify variance + information for their universes (in :ref:`Cumulative <cumulative>` + mode) (`#12653 <https://github.com/coq/coq/pull/12653>`_, by Gaëtan + Gilbert). + + .. _813UnusedVar: + +- **Added:** + Warning on unused variables in pattern-matching branches of + :n:`match` serving as catch-all branches for at least two distinct + patterns. + (`#12768 <https://github.com/coq/coq/pull/12768>`_, + fixes `#12762 <https://github.com/coq/coq/issues/12762>`_, + by Hugo Herbelin). +- **Added:** + Definition and (Co)Fixpoint now support the :attr:`using` attribute. + It has the same effect as :cmd:`Proof using`, which is only available in + interactive mode. + (`#13183 <https://github.com/coq/coq/pull/13183>`_, + by Enrico Tassi). + + .. _813TypingFlags: + +- **Added:** + Typing flags can now be specified per-constant / inductive, this + allows to fine-grain specify them from plugins or attributes. See + :ref:`controlling-typing-flags` for details on attribute syntax. + (`#12586 <https://github.com/coq/coq/pull/12586>`_, + by Emilio Jesus Gallego Arias). + +- **Added:** + Inference of return predicate of a :g:`match` by inversion takes + sort elimination constraints into account + (`#13290 <https://github.com/coq/coq/pull/13290>`_, + grants `#13278 <https://github.com/coq/coq/issues/13278>`_, + by Hugo Herbelin). +- **Fixed:** + Implicit arguments taken into account in defined fields of a record type declaration + (`#13166 <https://github.com/coq/coq/pull/13166>`_, + fixes `#13165 <https://github.com/coq/coq/issues/13165>`_, + by Hugo Herbelin). +- **Fixed:** + Allow use of typeclass inference for the return predicate of a :n:`match` + (was deactivated in versions 8.10 to 8.12, `#13217 <https://github.com/coq/coq/pull/13217>`_, + fixes `#13216 <https://github.com/coq/coq/issues/13216>`_, + by Hugo Herbelin). +- **Fixed:** + A case of unification raising an anomaly IllTypedInstance + (`#13376 <https://github.com/coq/coq/pull/13376>`_, + fixes `#13266 <https://github.com/coq/coq/issues/13266>`_, + by Hugo Herbelin). +- **Fixed:** + Using :n:`{wf ...}` in local fixpoints is an error, not an anomaly + (`#13383 <https://github.com/coq/coq/pull/13383>`_, + fixes `#11816 <https://github.com/coq/coq/issues/11816>`_, + by Hugo Herbelin). +- **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). +- **Fixed:** + A bug producing ill-typed instances of existential variables when let-ins + interleaved with assumptions + (`#13387 <https://github.com/coq/coq/pull/13387>`_, + fixes `#12348 <https://github.com/coq/coq/issues/13387>`_, + by Hugo Herbelin). + + .. _813Notations: + +Notations +^^^^^^^^^ + +- **Changed:** + In notations (except in custom entries), the misleading :n:`@syntax_modifier` + :n:`@ident ident` (which accepted either an identifier or + a :g:`_`) is deprecated and should be replaced by :n:`@ident name`. If + the intent was really to only parse identifiers, this will + eventually become possible, but only as of Coq 8.15. + In custom entries, the meaning of :n:`@ident ident` is silently changed + from parsing identifiers or :g:`_` to parsing only identifiers + without warning, but this presumably affects only rare, recent and + relatively experimental code + (`#11841 <https://github.com/coq/coq/pull/11841>`_, + fixes `#9514 <https://github.com/coq/coq/pull/9514>`_, + by Hugo Herbelin). +- **Changed:** + Improved support for notations/abbreviations with mixed terms and patterns (such as the forcing modality) + (`#12099 <https://github.com/coq/coq/pull/12099>`_, + by Hugo Herbelin). +- **Changed** + Rational and real constants are parsed differently. + The exponent is now encoded separately from the fractional part + using ``Z.pow_pos``. This way, parsing large exponents can no longer + blow up and constants are printed in a form closer to the one in which they + were parsed (i.e., ``102e-2`` is reprinted as such and not ``1.02``). + (`#12218 <https://github.com/coq/coq/pull/12218>`_, + by Pierre Roux). +- **Changed:** + Scope information is propagated in indirect applications to a + reference prefixed with :g:`@`; this covers for instance the case + :g:`r.(@p) t` where scope information from :g:`p` is now taken into + account for interpreting :g:`t` (`#12685 + <https://github.com/coq/coq/pull/12685>`_, by Hugo Herbelin). +- **Changed:** + New model for ``only parsing`` and ``only printing`` notations with + support for at most one parsing-and-printing or only-parsing + notation per notation and scope, but an arbitrary number of + only-printing notations + (`#12950 <https://github.com/coq/coq/pull/12950>`_, + fixes `#4738 <https://github.com/coq/coq/issues/4738>`_ + and `#9682 <https://github.com/coq/coq/issues/9682>`_ + and part 2 of `#12908 <https://github.com/coq/coq/issues/12908>`_, + by Hugo Herbelin). +- **Changed:** + Redeclaring a notation also reactivates 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 in 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). +- **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). +- **Removed** + OCaml parser and printer for real constants have been removed. + Real constants are now handled with proven Coq code. + (`#12218 <https://github.com/coq/coq/pull/12218>`_, + by Pierre Roux). +- **Deprecated** + ``Numeral.v`` is deprecated, please use ``Number.v`` instead. + (`#12218 <https://github.com/coq/coq/pull/12218>`_, + by Pierre Roux). +- **Deprecated:** + `Numeral Notation`, please use :cmd:`Number Notation` instead + (`#12979 <https://github.com/coq/coq/pull/12979>`_, + by Pierre Roux). +- **Added:** + :flag:`Printing Float` flag to print primitive floats as hexadecimal + instead of decimal values. This is included in the :flag:`Printing All` flag + (`#11986 <https://github.com/coq/coq/pull/11986>`_, + by Pierre Roux). +- **Added:** + :ref:`Number Notation <number-notations>` and :ref:`String Notation + <string-notations>` commands now + support parameterized inductive and non inductive types + (`#12218 <https://github.com/coq/coq/pull/12218>`_, + fixes `#12035 <https://github.com/coq/coq/issues/12035>`_, + by Pierre Roux, review by Jason Gross and Jim Fehrle for the + reference manual). +- **Added:** + Added support for encoding notations of the form :g:`x ⪯ y ⪯ .. ⪯ z ⪯ t`. + This feature is considered experimental. + (`#12765 <https://github.com/coq/coq/pull/12765>`_, + by Hugo Herbelin). +- **Added:** + The :n:`@binder` entry of :cmd:`Notation` can now be used in + notations expecting a single (non-recursive) binder + (`#13265 <https://github.com/coq/coq/pull/13265>`_, + by Hugo Herbelin, see section :ref:`notations-and-binders` of the + reference manual). +- **Fixed:** + Issues in the presence of notations recursively referring to another + applicative notations, such as missing scope propagation, or failure + to use a notation for printing + (`#12960 <https://github.com/coq/coq/pull/12960>`_, + fixes `#9403 <https://github.com/coq/coq/issues/9403>`_ + and `#10803 <https://github.com/coq/coq/issues/10803>`_, + by Hugo Herbelin). +- **Fixed:** + Capture the names 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). +- **Fixed:** + Preventing notations for constructors to involve binders + (`#13092 <https://github.com/coq/coq/pull/13092>`_, + fixes `#13078 <https://github.com/coq/coq/issues/13078>`_, + by Hugo Herbelin). +- **Fixed:** Notations understand universe names without getting + confused by different imported modules between declaration and use + locations (`#13415 <https://github.com/coq/coq/pull/13415>`_, fixes + `#13303 <https://github.com/coq/coq/issues/13303>`_, by Gaëtan + Gilbert). + + .. _813Tactics: + +Tactics +^^^^^^^ + +- **Changed:** + In :tacn:`refine`, new existential variables unified with existing ones are no + longer considered as fresh. The behavior of :tacn:`simple refine` no longer depends on + the orientation of evar-evar unification problems, and new existential variables + are always turned into (unshelved) goals. This can break compatibility in + some cases (`#7825 <https://github.com/coq/coq/pull/7825>`_, by Matthieu + Sozeau, with help from Maxime Dénès, review by Pierre-Marie Pédrot and + Enrico Tassi, fixes `#4095 <https://github.com/coq/coq/issues/4095>`_ and + `#4413 <https://github.com/coq/coq/issues/4413>`_). +- **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). +- **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). +- **Removed:** + A number of tactics that formerly accepted negative + numbers as parameters now give syntax errors for negative + values. These include {e}constructor, do, timeout, + 9 {e}auto tactics and psatz*. + (`#13417 <https://github.com/coq/coq/pull/13417>`_, + by Jim Fehrle). +- **Removed:** + The deprecated and undocumented `prolog` tactic was removed + (`#12399 <https://github.com/coq/coq/pull/12399>`_, + by Pierre-Marie Pédrot). +- **Removed:** `info` tactic that was deprecated in 8.5. + (`#12423 <https://github.com/coq/coq/pull/12423>`_, by Jim Fehrle). +- **Deprecated:** + Undocumented :n:`eauto @nat_or_var @nat_or_var` syntax in favor of new :tacn:`bfs eauto`. + Also deprecated 2-integer syntax for :tacn:`debug eauto` and :tacn:`info_eauto`. + (Use :tacn:`bfs eauto` with the :flag:`Info Eauto` or :flag:`Debug Eauto` flags instead.) + (`#13381 <https://github.com/coq/coq/pull/13381>`_, + by Jim Fehrle). +- **Added:** + :tacn:`lia` is extended to deal with boolean operators e.g. `andb` or `Z.leb`. + (As `lia` gets more powerful, this may break proof scripts relying on `lia` failure.) + (`#11906 <https://github.com/coq/coq/pull/11906>`_, by Frédéric Besson). +- **Added:** + :tacn:`apply … in` supports several hypotheses + (`#12246 <https://github.com/coq/coq/pull/12246>`_, + by Hugo Herbelin; grants + `#9816 <https://github.com/coq/coq/pull/9816>`_). +- **Added:** + The :tacn:`zify` tactic can now be extended by redefining the `zify_pre_hook` + tactic. (`#12552 <https://github.com/coq/coq/pull/12552>`_, + by Kazuhiko Sakaguchi). +- **Added:** + The :tacn:`zify` tactic provides support for primitive integers (module :g:`ZifyInt63`). + (`#12648 <https://github.com/coq/coq/pull/12648>`_, by Frédéric Besson). +- **Fixed:** + Avoid exposing an internal name of the form :n:`_tmp` when applying the + :n:`_` introduction pattern which would break a dependency + (`#13337 <https://github.com/coq/coq/pull/13337>`_, + fixes `#13336 <https://github.com/coq/coq/issues/13336>`_, + by Hugo Herbelin). +- **Fixed:** + The case of tactics, such as :tacn:`eapply`, producing existential variables + under binders with an ill-formed instance + (`#13373 <https://github.com/coq/coq/pull/13373>`_, + fixes `#13363 <https://github.com/coq/coq/issues/13363>`_, + by Hugo Herbelin). + +Tactic language +^^^^^^^^^^^^^^^ + +- **Added:** + An if-then-else syntax to Ltac2 + (`#13232 <https://github.com/coq/coq/pull/13232>`_, + fixes `#10110 <https://github.com/coq/coq/issues/10110>`_, + by Pierre-Marie Pédrot). +- **Fixed:** + Printing of the quotation qualifiers when printing :g:`Ltac` functions + (`#13028 <https://github.com/coq/coq/pull/13028>`_, + fixes `#9716 <https://github.com/coq/coq/issues/9716>`_ + and `#13004 <https://github.com/coq/coq/issues/13004>`_, + by Hugo Herbelin). + +SSReflect +^^^^^^^^^ + +- **Added:** + SSReflect intro pattern ltac views ``/[dup]``, ``/[swap]`` and ``/[apply]`` + (`#13317 <https://github.com/coq/coq/pull/13317>`_, + by Cyril Cohen). +- **Fixed:** + Working around a bug of interaction between + and /(ltac:(...)) cf + `#13458 <https://github.com/coq/coq/issues/13458>`_ + (`#13459 <https://github.com/coq/coq/pull/13459>`_, + by Cyril Cohen). + +Commands and options +^^^^^^^^^^^^^^^^^^^^ + +- **Changed:** + Drop prefixes from grammar non-terminal names, + e.g. "constr:global" -> "global", "Prim.name" -> "name". + Visible in the output of :cmd:`Print Grammar` and :cmd:`Print Custom Grammar`. + (`#13096 <https://github.com/coq/coq/pull/13096>`_, + by Jim Fehrle). +- **Changed:** + When declaring arbitrary terms as hints, unsolved + evars are not abstracted implicitly anymore and instead + raise an error + (`#13139 <https://github.com/coq/coq/pull/13139>`_, + by Pierre-Marie Pédrot). +- **Removed:** + In the :cmd:`Extraction Language` command, remove `Ocaml` as a valid value. + Use `OCaml` instead. This was deprecated in Coq 8.8, `#6261 <https://github.com/coq/coq/pull/6261>`_ + (`#13016 <https://github.com/coq/coq/pull/13016>`_, by Jim Fehrle). + + .. _813HintWarning: + +- **Deprecated:** + Hint locality currently defaults to :attr:`local` in a section and + :attr:`global` otherwise, but this will change in a future release. + Hints added outside of sections without an explicit + locality now generate a deprecation warning. We recommend + using :attr:`export` where possible + (`#13384 <https://github.com/coq/coq/pull/13384>`_, + by Pierre-Marie Pédrot). +- **Deprecated:** + :cmd:`Grab Existential Variables` and :cmd:`Existential` commands + (`#12516 <https://github.com/coq/coq/pull/12516>`_, + by Maxime Dénès). +- **Added:** + The :attr:`export` locality can now be used for all Hint commands, + including :cmd:`Hint Cut`, :cmd:`Hint Mode`, :cmd:`Hint Transparent` / + :cmd:`Opaque <Hint Opaque>` and + :cmd:`Remove Hints` + (`#13388 <https://github.com/coq/coq/pull/13388>`_, + by Pierre-Marie Pédrot). +- **Added:** + Support for automatic insertion of coercions in :cmd:`Search` + patterns. Additionally, head patterns are now automatically + interpreted as types + (`#13255 <https://github.com/coq/coq/pull/13255>`_, + fixes `#13244 <https://github.com/coq/coq/issues/13244>`_, + by Hugo Herbelin). +- **Added:** + The :cmd:`Proof using` command can now be used without loading the + Ltac plugin (`-noinit` mode) + (`#13339 <https://github.com/coq/coq/pull/13339>`_, + by Théo Zimmermann). +- **Added:** + Clarify in the documentation that :cmd:`Add ML Path` is not exported to compiled files + (`#13345 <https://github.com/coq/coq/pull/13345>`_, + fixes `#13344 <https://github.com/coq/coq/issues/13344>`_, + by Hugo Herbelin). + +Tools +^^^^^ + +- **Changed:** + Option `-native-compiler` of the configure script now impacts the + default value of the `-native-compiler` option of coqc. The + `-native-compiler` option of the configure script supports a new `ondemand` + value, which becomes the default, thus preserving the previous default + behavior. + The stdlib is still precompiled when configuring with `-native-compiler + yes`. It is not precompiled otherwise. + This an implementation of point 2 of + `CEP #48 <https://github.com/coq/ceps/pull/48>`_ + (`#13352 <https://github.com/coq/coq/pull/13352>`_, + by Pierre Roux). +- **Changed:** + Added the ability for coq_makefile to directly set the installation folders, + through the `COQLIBINSTALL` and `COQDOCINSTALL` variables. + See :ref:`coqmakefilelocal`. + (`#12389 <https://github.com/coq/coq/pull/12389>`_, by Martin Bodin, review of Enrico Tassi). +- **Removed:** The option ``-I`` of coqchk was removed (it was + deprecated in Coq 8.8) (`#12613 + <https://github.com/coq/coq/pull/12613>`_, by Gaëtan Gilbert). +- **Fixed:** + ``coqchk`` no longer reports names from inner modules of opaque modules as + axioms (`#12862 <https://github.com/coq/coq/pull/12862>`_, fixes `#12845 + <https://github.com/coq/coq/issues/12845>`_, by Jason Gross). + +CoqIDE +^^^^^^ + +- **Added:** + Support showing diffs for :cmd:`Show Proof` in CoqIDE from the :n:`View` menu. + See :ref:`showing_proof_diffs`. + (`#12874 <https://github.com/coq/coq/pull/12874>`_, + by Jim Fehrle and Enrico Tassi) +- **Added:** + Support for flag :flag:`Printing Goal Names` in View menu + (`#13145 <https://github.com/coq/coq/pull/13145>`_, + by Hugo Herbelin). + +Standard library +^^^^^^^^^^^^^^^^ + +- **Changed:** + In the reals theory changed the epsilon in the definition of the modulus of convergence for CReal from 1/n (n in positive) to 2^z (z in Z) + so that a precision coarser than one is possible. Also added an upper bound to CReal to enable more efficient computations. + (`#12186 <https://github.com/coq/coq/pull/12186>`_, + by Michael Soegtrop). +- **Changed:** + Int63 notations now match up with the rest of the standard library: :g:`a \% + m`, :g:`m == n`, :g:`m < n`, :g:`m <= n`, and :g:`m ≤ n` have been replaced + with :g:`a mod m`, :g:`m =? n`, :g:`m <? n`, :g:`m <=? n`, and :g:`m ≤? n`. + The old notations are still available as deprecated notations. Additionally, + there is now a ``Coq.Numbers.Cyclic.Int63.Int63.Int63Notations`` module that + users can import to get the ``Int63`` notations without unqualifying the + various primitives (`#12479 <https://github.com/coq/coq/pull/12479>`_, fixes + `#12454 <https://github.com/coq/coq/issues/12454>`_, by Jason Gross). +- **Changed:** + PrimFloat notations now match up with the rest of the standard library: :g:`m + == n`, :g:`m < n`, and :g:`m <= n` have been replaced with :g:`m =? n`, :g:`m + <? n`, and :g:`m <=? n`. The old notations are still available as deprecated + notations. Additionally, there is now a + ``Coq.Floats.PrimFloat.PrimFloatNotations`` module that users can import to + get the ``PrimFloat`` notations without unqualifying the various primitives + (`#12556 <https://github.com/coq/coq/pull/12556>`_, fixes `#12454 + <https://github.com/coq/coq/issues/12454>`_, by Jason Gross). +- **Changed:** the sort of cyclic numbers from Type to Set. + For backward compatibility, a dynamic sort was defined in the 3 packages bignums, coqprime and color. + See for example commit 6f62bda in bignums. + (`#12801 <https://github.com/coq/coq/pull/12801>`_, + by Vincent Semeria). +- **Changed:** + ``Require Import Coq.nsatz.NsatzTactic`` now allows using :tacn:`nsatz` + with `Z` and `Q` without having to supply instances or using ``Require Import Coq.nsatz.Nsatz``, which + transitively requires unneeded files declaring axioms used in the reals + (`#12861 <https://github.com/coq/coq/pull/12861>`_, + fixes `#12860 <https://github.com/coq/coq/issues/12860>`_, + by Jason Gross). +- **Deprecated:** + ``prod_curry`` and ``prod_uncurry``, in favor of ``uncurry`` and ``curry`` + (`#12716 <https://github.com/coq/coq/pull/12716>`_, + by Yishuai Li). +- **Added:** + New lemmas about ``repeat`` in ``List`` and ``Permutation``: ``repeat_app``, ``repeat_eq_app``, ``repeat_eq_cons``, ``repeat_eq_elt``, ``Forall_eq_repeat``, ``Permutation_repeat`` + (`#12799 <https://github.com/coq/coq/pull/12799>`_, + by Olivier Laurent). +- **Added:** + Extend some list lemmas to both directions: `app_inj_tail_iff`, `app_inv_head_iff`, `app_inv_tail_iff`. + (`#12094 <https://github.com/coq/coq/pull/12094>`_, + fixes `#12093 <https://github.com/coq/coq/issues/12093>`_, + by Edward Wang). +- **Added:** + ``Decidable`` instance for negation + (`#12420 <https://github.com/coq/coq/pull/12420>`_, + by Yishuai Li). +- **Fixed:** + `Coq.Program.Wf.Fix_F_inv` and `Coq.Program.Wf.Fix_eq` are now axiom-free. They no longer assume proof irrelevance. + (`#13365 <https://github.com/coq/coq/pull/13365>`_, + by Li-yao Xia). + +Infrastructure and dependencies +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +- **Changed:** + When compiled with OCaml >= 4.10.0, Coq will use the new best-fit GC + policy, which should provide some performance benefits. Coq's policy + is optimized for speed, but could increase memory consumption in + some cases. You are welcome to tune it using the ``OCAMLRUNPARAM`` + variable and report back on good settings so we can improve the defaults. + (`#13040 <https://github.com/coq/coq/pull/13040>`_, + fixes `#11277 <https://github.com/coq/coq/issues/11277>`_, + by Emilio Jesus Gallego Arias). +- **Changed:** + Coq now uses the `zarith <https://github.com/ocaml/Zarith>`_ + library, based on GNU's gmp instead of ``num`` which is + deprecated upstream. The custom ``bigint`` module is + no longer provided. + (`#11742 <https://github.com/coq/coq/pull/11742>`_, + `#13007 <https://github.com/coq/coq/pull/13007>`_, + by Emilio Jesus Gallego Arias and Vicent Laporte, with help from + Frédéric Besson). + +Changes in 8.13.0 +~~~~~~~~~~~~~~~~~ + +Commands and options +^^^^^^^^^^^^^^^^^^^^ + +- **Changed:** + The warning `custom-entry-overriden` has been renamed to `custom-entry-overridden` (with two d's). + (`#13556 <https://github.com/coq/coq/pull/13556>`_, + by Simon Friis Vindum). + +Changes in 8.13.1 +~~~~~~~~~~~~~~~~~ + +Kernel +^^^^^^ + +- **Fixed:** + Fix arities of VM opcodes for some floating-point operations + that could cause memory corruption + (`#13867 <https://github.com/coq/coq/pull/13867>`_, + by Guillaume Melquiond). + +CoqIDE +^^^^^^ + +- **Added:** + Option ``-v`` and ``--version`` to CoqIDE + (`#13870 <https://github.com/coq/coq/pull/13870>`_, + by Guillaume Melquiond). + + Version 8.12 ------------ @@ -261,7 +975,7 @@ Notations by Hugo Herbelin). - **Fixed:** Different interpretations in different scopes of the same notation - string can now be associated to different printing formats (`#10832 + string can now be associated with different printing formats (`#10832 <https://github.com/coq/coq/pull/10832>`_, by Hugo Herbelin, fixes `#6092 <https://github.com/coq/coq/issues/6092>`_ and `#7766 <https://github.com/coq/coq/issues/7766>`_). @@ -537,7 +1251,7 @@ Flags, options and attributes :attr:`universes(template)` and ``universes(notemplate)`` instead (`#11663 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann). - **Deprecated:** - :flag:`Hide Obligations` flag + `Hide Obligations` flag (`#11828 <https://github.com/coq/coq/pull/11828>`_, by Emilio Jesus Gallego Arias). - **Added:** Handle the :attr:`local` attribute in :cmd:`Canonical @@ -608,7 +1322,7 @@ Commands Declaration of arbitrary terms as hints. Global references are now preferred (`#7791 <https://github.com/coq/coq/pull/7791>`_, by Pierre-Marie Pédrot). -- **Deprecated:** :cmd:`SearchHead` in favor of the new `headconcl:` +- **Deprecated:** `SearchHead` in favor of the new `headconcl:` clause of :cmd:`Search` (part of `#8855 <https://github.com/coq/coq/pull/8855>`_, by Théo Zimmermann). - **Added:** @@ -1336,6 +2050,25 @@ Changes in 8.12.1 fixes `#12332 <https://github.com/coq/coq/issues/12332>`_, by Théo Zimmermann and Jim Fehrle). +Changes in 8.12.2 +~~~~~~~~~~~~~~~~~ + +**Notations** + +- **Fixed:** + 8.12 regression causing notations mentioning a coercion to be ignored + (`#13436 <https://github.com/coq/coq/pull/13436>`_, + fixes `#13432 <https://github.com/coq/coq/issues/13432>`_, + by Hugo Herbelin). + +**Tactics** + +- **Fixed:** + 8.12 regression: incomplete inference of implicit arguments in :tacn:`exists` + (`#13468 <https://github.com/coq/coq/pull/13468>`_, + fixes `#13456 <https://github.com/coq/coq/issues/13456>`_, + by Hugo Herbelin). + Version 8.11 ------------ @@ -1521,7 +2254,7 @@ Changes in 8.11+beta1 documentation. (`#10441 <https://github.com/coq/coq/pull/10441>`_, by Pierre-Marie Pédrot) - **Added:** - The :cmd:`Section` vernacular command now accepts the "universes" attribute. In + The :cmd:`Section` command now accepts the "universes" attribute. In addition to setting the section universe polymorphism, it also locally sets the universe polymorphic option inside the section. (`#10441 <https://github.com/coq/coq/pull/10441>`_, by Pierre-Marie Pédrot) @@ -2479,7 +3212,7 @@ Other changes in 8.10+beta1 by Maxime Dénès, review by Pierre-Marie Pédrot). - New variant :tacn:`change_no_check` of :tacn:`change`, usable as a - documented replacement of :tacn:`convert_concl_no_check` + documented replacement of `convert_concl_no_check` (`#10012 <https://github.com/coq/coq/pull/10012>`_, `#10017 <https://github.com/coq/coq/pull/10017>`_, `#10053 <https://github.com/coq/coq/pull/10053>`_, and @@ -2520,7 +3253,7 @@ Other changes in 8.10+beta1 New `relpre R f` definition for the preimage of a relation R under f (`#9995 <https://github.com/coq/coq/pull/9995>`_, by Georges Gonthier). -- Vernacular commands: +- Commands: - Binders for an :cmd:`Instance` now act more like binders for a :cmd:`Theorem`. Names may not be repeated, and may not overlap with section variable names @@ -2852,7 +3585,7 @@ Changes in 8.10.2 **Notations** -- Fixed an 8.10 regression related to the printing of coercions associated to notations +- Fixed an 8.10 regression related to the printing of coercions associated with notations (`#11090 <https://github.com/coq/coq/pull/11090>`_, fixes `#11033 <https://github.com/coq/coq/issues/11033>`_, by Hugo Herbelin). @@ -3093,7 +3826,7 @@ Focusing - Focusing bracket `{` now supports named goal selectors, e.g. `[x]: {` will focus on a goal (existential variable) named `x`. - As usual, unfocus with `}` once the sub-goal is fully solved. + As usual, unfocus with `}` once the subgoal is fully solved. Specification language @@ -3158,7 +3891,7 @@ Tools please open an issue. We can help set up external maintenance as part of Proof-General, or independently as part of coq-community. -Vernacular Commands +Commands - Removed deprecated commands `Arguments Scope` and `Implicit Arguments` (not the option). Use the `Arguments` command instead. @@ -3429,11 +4162,11 @@ Tactics Focusing - Focusing bracket `{` now supports single-numbered goal selector, - e.g. `2: {` will focus on the second sub-goal. As usual, unfocus - with `}` once the sub-goal is fully solved. + e.g. `2: {` will focus on the second subgoal. As usual, unfocus + with `}` once the subgoal is fully solved. The `Focus` and `Unfocus` commands are now deprecated. -Vernacular Commands +Commands - Proofs ending in "Qed exporting ident, .., ident" are not supported anymore. Constants generated during `abstract` are kept private to the @@ -3807,7 +4540,7 @@ Gallina - Now supporting all kinds of binders, including 'pat, in syntax of record fields. -Vernacular Commands +Commands - Goals context can be printed in a more compact way when `Set Printing Compact Contexts` is activated. @@ -4639,7 +5372,7 @@ Logic the dependent one. To recover the old behavior, explicitly define your inductive types in Set. -Vernacular commands +Commands - A command "Variant" allows to define non-recursive variant types. - The command "Record foo ..." does not generate induction principles @@ -5096,7 +5829,7 @@ API Details of changes in 8.5beta3 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Vernacular commands +Commands - New command "Redirect" to redirect the output of a command to a file. - New command "Undelimit Scope" to remove the delimiter of a scope. @@ -5475,7 +6208,7 @@ Regarding decision tactics, Loïc Pottier maintained nsatz, moving in particular to a typeclass based reification of goals while Frédéric Besson maintained Micromega, adding in particular support for division. -Regarding vernacular commands, Stéphane Glondu provided new commands to +Regarding commands, Stéphane Glondu provided new commands to analyze the structure of type universes. Regarding libraries, a new library about lists of a given length (called @@ -5672,7 +6405,7 @@ Tactics constructor. Last one can mark a constant so that it is unfolded only if the simplified term does not expose a match in head position. -Vernacular commands +Commands - It is now mandatory to have a space (or tabulation or newline or end-of-file) after a "." ending a sentence. @@ -5862,7 +6595,7 @@ Tools Details of changes in 8.4beta2 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Vernacular commands +Commands - Commands "Back" and "BackTo" are now handling the proof states. They may perform some extra steps of backtrack to avoid states where the proof @@ -5911,7 +6644,7 @@ CoqIDE Details of changes in 8.4 ~~~~~~~~~~~~~~~~~~~~~~~~~ -Vernacular commands +Commands - The "Reset" command is now supported again in files given to coqc or Load. - "Show Script" now indents again the displayed scripts. It can also work @@ -6215,7 +6948,7 @@ Type classes anonymous instances, declarations giving terms, better handling of sections and [Context]. -Vernacular commands +Commands - New command "Timeout <n> <command>." interprets a command and a timeout interrupts the execution after <n> seconds. @@ -6388,7 +7121,7 @@ implement a new resolution-based version of the tactics dedicated to rewriting on arbitrary transitive relations. Another major improvement of Coq 8.2 is the evolution of the arithmetic -libraries and of the tools associated to them. Benjamin Grégoire and +libraries and of the tools associated with them. Benjamin Grégoire and Laurent Théry contributed a modular library for building arbitrarily large integers from bounded integers while Evgeny Makarov contributed a modular library of abstract natural and integer arithmetic together @@ -6496,7 +7229,7 @@ Language of easily fixed incompatibility in case of manual definition of a recursor in a recursive singleton inductive type]. -Vernacular commands +Commands - Added option Global to "Arguments Scope" for section surviving. - Added option "Unset Elimination Schemes" to deactivate the automatic @@ -7096,7 +7829,7 @@ Syntax - Support for primitive interpretation of string literals - Extended support for Unicode ranges -Vernacular commands +Commands - Added "Print Ltac qualid" to print a user defined tactic. - Added "Print Rewrite HintDb" to print the content of a DB used by @@ -7274,7 +8007,7 @@ Libraries - Acc in Wf.v and clos_refl_trans in Relation_Operators.v now rely on the allowance for recursively non uniform parameters (possible source of incompatibilities: explicit pattern-matching on these - types may require to remove the occurrence associated to their + types may require to remove the occurrence associated with their recursively non uniform parameter). - Coq.List.In_dec has been set transparent (this may exceptionally break proof scripts, set it locally opaque for compatibility). @@ -7493,7 +8226,7 @@ Syntax for arithmetic - Locate applied to a simple string (e.g. "+") searches for all notations containing this string -Vernacular commands +Commands - "Declare ML Module" now allows to import .cma files. This avoids to use a bunch of "Declare ML Module" statements when using several ML files. @@ -7654,7 +8387,7 @@ New concrete syntax - A completely new syntax for terms - A more uniform syntax for tactics and the tactic language -- A few syntactic changes for vernacular commands +- A few syntactic changes for commands - A smart automatic translator translating V8.0 files in old syntax to files valid for V8.0 @@ -7725,7 +8458,7 @@ Known problems of the automatic translation Details of changes in 8.0 ~~~~~~~~~~~~~~~~~~~~~~~~~ -Vernacular commands +Commands - New option "Set Printing All" to deactivate all high-level forms of printing (implicit arguments, coercions, destructing let, diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 246568d3c1..edbc89aad8 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -183,11 +183,8 @@ todo_include_todos = False nitpicky = True nitpick_ignore = [ ('token', token) for token in [ - 'tactic', 'induction_clause', - 'conversion', 'where', - 'oriented_rewriter', 'bindings_with_parameters', 'destruction_arg' ]] @@ -220,7 +217,7 @@ html_context = { ("dev", "https://coq.github.io/doc/master/refman/"), ("stable", "https://coq.inria.fr/distrib/current/refman/"), ("v8.13", "https://coq.github.io/doc/v8.13/refman/"), - ("8.12", "https://coq.inria.fr/distrib/V8.12.1/refman/"), + ("8.12", "https://coq.inria.fr/distrib/V8.12.2/refman/"), ("8.11", "https://coq.inria.fr/distrib/V8.11.2/refman/"), ("8.10", "https://coq.inria.fr/distrib/V8.10.2/refman/"), ("8.9", "https://coq.inria.fr/distrib/V8.9.1/refman/"), @@ -493,3 +490,6 @@ epub_exclude_files = ['search.html'] # navtree options navtree_shift = True + +# since sphinxcontrib-bibtex version 2 we need this +bibtex_bibfiles = [ "biblio.bib" ] diff --git a/doc/sphinx/history.rst b/doc/sphinx/history.rst index c5ef92a1bf..44f2d23801 100644 --- a/doc/sphinx/history.rst +++ b/doc/sphinx/history.rst @@ -954,7 +954,7 @@ Parsing and grammar extension for Time and to write grammar rules abbreviating several commands) (+) - The default parser for actions in the grammar rules (and for - patterns in the pretty-printing rules) is now the one associated to + patterns in the pretty-printing rules) is now the one associated with the grammar (i.e. vernac, tactic or constr); no need then for quotations as in <:vernac:<...>>; to return an "ast", the grammar must be explicitly typed with tag ": ast" or ": ast list", or if a @@ -1346,12 +1346,12 @@ Language instead to simulate the old behaviour of Local (the section part of the name is not kept though) -ML tactic and vernacular commands +ML tactics and commands - "Grammar tactic" and "Grammar vernac" of type "ast" are no longer supported (only "Grammar tactic simple_tactic" of type "tactic" remains available). -- Concrete syntax for ML written vernacular commands and tactics is +- Concrete syntax for ML written commands and tactics is now declared at ML level using camlp4 macros TACTIC EXTEND et VERNAC COMMAND EXTEND. - "Check n c" now "n:Check c", "Eval n ..." now "n:Eval ..." diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 06a677d837..0b183d3f3f 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -45,9 +45,9 @@ This manual is organized in three main parts, plus an appendix: translated down to the language of the kernel by means of an "elaboration process". -- **The second part presents the interactive proof mode**, the central +- **The second part presents proof mode**, the central feature of Coq. :ref:`writing-proofs` introduces this interactive - proof mode and the available proof languages. + mode and the available proof languages. :ref:`automatic-tactics` presents some more advanced tactics, while :ref:`writing-tactics` is about the languages that allow a user to combine tactics together and develop new ones. diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 85b04f6df0..1cfd8dac50 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -101,7 +101,7 @@ and it can be applied to any expression of type :math:`\nat`, say :math:`t`, to object :math:`P~t` of type :math:`\Prop`, namely a proposition. Furthermore :g:`forall x:nat, P x` will represent the type of functions -which associate to each natural number :math:`n` an object of type :math:`(P~n)` and +which associate with each natural number :math:`n` an object of type :math:`(P~n)` and consequently represent the type of proofs of the formula “:math:`∀ x.~P(x)`”. @@ -111,51 +111,49 @@ Typing rules ---------------- As objects of type theory, terms are subjected to *type discipline*. -The well typing of a term depends on a global environment and a local -context. - +The well typing of a term depends on a local context and a global environment. .. _Local-context: **Local context.** -A *local context* is an ordered list of *local declarations* of names -which we call *variables*. The declaration of some variable :math:`x` is -either a *local assumption*, written :math:`x:T` (:math:`T` is a type) or a *local -definition*, written :math:`x:=t:T`. We use brackets to write local contexts. -A typical example is :math:`[x:T;~y:=u:U;~z:V]`. Notice that the variables +A :term:`local context` is an ordered list of declarations of *variables*. +The declaration of a variable :math:`x` is +either an *assumption*, written :math:`x:T` (where :math:`T` is a type) or a +*definition*, written :math:`x:=t:T`. Local contexts are written in brackets, +for example :math:`[x:T;~y:=u:U;~z:V]`. The variables declared in a local context must be distinct. If :math:`Γ` is a local context -that declares some :math:`x`, we -write :math:`x ∈ Γ`. By writing :math:`(x:T) ∈ Γ` we mean that either :math:`x:T` is an -assumption in :math:`Γ` or that there exists some :math:`t` such that :math:`x:=t:T` is a -definition in :math:`Γ`. If :math:`Γ` defines some :math:`x:=t:T`, we also write :math:`(x:=t:T) ∈ Γ`. +that declares :math:`x`, we +write :math:`x ∈ Γ`. Writing :math:`(x:T) ∈ Γ` means there is an assumption +or a definition giving the type :math:`T` to :math:`x` in :math:`Γ`. +If :math:`Γ` defines :math:`x:=t:T`, we also write :math:`(x:=t:T) ∈ Γ`. For the rest of the chapter, :math:`Γ::(y:T)` denotes the local context :math:`Γ` enriched with the local assumption :math:`y:T`. Similarly, :math:`Γ::(y:=t:T)` denotes the local context :math:`Γ` enriched with the local definition :math:`(y:=t:T)`. The -notation :math:`[]` denotes the empty local context. By :math:`Γ_1 ; Γ_2` we mean +notation :math:`[]` denotes the empty local context. Writing :math:`Γ_1 ; Γ_2` means concatenation of the local context :math:`Γ_1` and the local context :math:`Γ_2`. - .. _Global-environment: **Global environment.** -A *global environment* is an ordered list of *global declarations*. -Global declarations are either *global assumptions* or *global -definitions*, but also declarations of inductive objects. Inductive -objects themselves declare both inductive or coinductive types and -constructors (see Section :ref:`inductive-definitions`). - -A *global assumption* will be represented in the global environment as -:math:`(c:T)` which assumes the name :math:`c` to be of some type :math:`T`. A *global -definition* will be represented in the global environment as :math:`c:=t:T` -which defines the name :math:`c` to have value :math:`t` and type :math:`T`. We shall call +A :term:`global environment` is an ordered list of *declarations*. +Global declarations are either *assumptions*, *definitions* +or declarations of inductive objects. Inductive +objects declare both constructors and inductive or +coinductive types (see Section :ref:`inductive-definitions`). + +In the global environment, +*assumptions* are written as +:math:`(c:T)`, indicating that :math:`c` is of the type :math:`T`. *Definitions* +are written as :math:`c:=t:T`, indicating that :math:`c` has the value :math:`t` +and type :math:`T`. We shall call such names *constants*. For the rest of the chapter, the :math:`E;~c:T` denotes -the global environment :math:`E` enriched with the global assumption :math:`c:T`. +the global environment :math:`E` enriched with the assumption :math:`c:T`. Similarly, :math:`E;~c:=t:T` denotes the global environment :math:`E` enriched with the -global definition :math:`(c:=t:T)`. +definition :math:`(c:=t:T)`. The rules for inductive definitions (see Section :ref:`inductive-definitions`) have to be considered as assumption -rules to which the following definitions apply: if the name :math:`c` +rules in which the following definitions apply: if the name :math:`c` is declared in :math:`E`, we write :math:`c ∈ E` and if :math:`c:T` or :math:`c:=t:T` is declared in :math:`E`, we write :math:`(c : T) ∈ E`. @@ -315,7 +313,7 @@ following rules. .. note:: We may have :math:`\letin{x}{t:T}{u}` well-typed without having :math:`((λ x:T.~u)~t)` well-typed (where :math:`T` is a type of - :math:`t`). This is because the value :math:`t` associated to + :math:`t`). This is because the value :math:`t` associated with :math:`x` may be used in a conversion rule (see Section :ref:`Conversion-rules`). diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index d061ed41f1..4f54e33758 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -902,7 +902,6 @@ In addition to the powerful ``ring``, ``field`` and ``lra`` tactics (see Chapter :ref:`tactics`), there are also: .. tacn:: discrR - :name: discrR Proves that two real integer constants are different. @@ -916,7 +915,6 @@ tactics (see Chapter :ref:`tactics`), there are also: discrR. .. tacn:: split_Rabs - :name: split_Rabs Allows unfolding the ``Rabs`` constant and splits corresponding conjunctions. @@ -930,7 +928,6 @@ tactics (see Chapter :ref:`tactics`), there are also: intro; split_Rabs. .. tacn:: split_Rmult - :name: split_Rmult Splits a condition that a product is non null into subgoals corresponding to the condition on each operand of the product. diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index e029068630..7566996ef6 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/doc/sphinx/language/core/assumptions.rst @@ -9,7 +9,7 @@ Binders .. insertprodn open_binders binder .. prodn:: - open_binders ::= {+ @name } : @term + open_binders ::= {+ @name } : @type | {+ @binder } name ::= _ | @ident @@ -115,10 +115,10 @@ Section :ref:`explicit-applications`). Assumptions ----------- -Assumptions extend the environment with axioms, parameters, hypotheses +Assumptions extend the global environment with axioms, parameters, hypotheses or variables. An assumption binds an :n:`@ident` to a :n:`@type`. It is accepted -by Coq if and only if this :n:`@type` is a correct type in the environment -preexisting the declaration and if :n:`@ident` was not previously defined in +by Coq only if :n:`@type` is a correct type in the global environment +before the declaration and if :n:`@ident` was not previously defined in the same module. This :n:`@type` is considered to be the type (or specification, or statement) assumed by :n:`@ident` and we say that :n:`@ident` has type :n:`@type`. @@ -141,7 +141,7 @@ has type :n:`@type`. of_type ::= {| : | :> } @type These commands bind one or more :n:`@ident`\(s) to specified :n:`@type`\(s) as their specifications in - the global context. The fact asserted by :n:`@type` (or, equivalently, the existence + the global environment. The fact asserted by :n:`@type` (or, equivalently, the existence of an object of this type) is accepted as a postulate. They accept the :attr:`program` attribute. :cmd:`Axiom`, :cmd:`Conjecture`, :cmd:`Parameter` and their plural forms @@ -170,7 +170,7 @@ has type :n:`@type`. Axiom R_S_inv : forall x y, R x y <-> S y x. .. exn:: @ident already exists. - :name: @ident already exists. (Axiom) + :name: ‘ident’ already exists. (Axiom) :undocumented: .. warn:: @ident is declared as a local axiom diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 2b262b89c0..2b50d4c420 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -64,7 +64,7 @@ appending the level to the nonterminal name (as in :n:`@term100` or populated by notations or plugins. Furthermore, some parsing rules are only activated in certain - contexts (:ref:`interactive proof mode <proofhandling>`, + contexts (:ref:`proof mode <proofhandling>`, :ref:`custom entries <custom-entries>`...). .. warning:: @@ -332,9 +332,9 @@ rest of the Coq manual: :term:`terms <term>` and :term:`types tactic - Tactics specify how to transform the current proof state as a + A :production:`tactic` specifies how to transform the current proof state as a step in creating a proof. They are syntactically valid only when - Coq is in proof mode, such as after a :cmd:`Theorem` command + Coq is in :term:`proof mode`, such as after a :cmd:`Theorem` command and before any subsequent proof-terminating command such as :cmd:`Qed`. See :ref:`proofhandling` for more on proof mode. @@ -450,7 +450,6 @@ they appear after a boldface label. They are listed in the :ref:`options_index`. .. cmd:: Set @setting_name {? {| @integer | @string } } - :name: Set If :n:`@setting_name` is a flag, no value may be provided; the flag is set to on. @@ -471,7 +470,6 @@ they appear after a boldface label. They are listed in the Coq versions. .. cmd:: Unset @setting_name - :name: Unset If :n:`@setting_name` is a flag, it is set to off. If :n:`@setting_name` is an option, it is set to its default value. @@ -525,31 +523,20 @@ they appear after a boldface label. They are listed in the Locality attributes supported by :cmd:`Set` and :cmd:`Unset` ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -The :cmd:`Set` and :cmd:`Unset` commands support the :attr:`local`, -:attr:`global` and :attr:`export` locality attributes: - -* no attribute: the original setting is *not* restored at the end of - the current module or section. -* :attr:`local` (or alternatively, the ``Local`` prefix): the setting - is applied within the current module or section. The original value - of the setting is restored at the end of the current module or - section. -* :attr:`export` (or alternatively, the ``Export`` prefix): similar to - :attr:`local`, the original value of the setting is restored at the - end of the current module or section. In addition, if the value is - set in a module, then :cmd:`Import`\-ing the module sets the option - or flag. -* :attr:`global` (or alternatively, the ``Global`` prefix): the - original setting is *not* restored at the end of the current module - or section. In addition, if the value is set in a file, then - :cmd:`Require`\-ing the file sets the option. +The :cmd:`Set` and :cmd:`Unset` commands support the mutually +exclusive :attr:`local`, :attr:`export` and :attr:`global` locality +attributes (or the ``Local``, ``Export`` or ``Global`` prefixes). + +If no attribute is specified, the original value of the flag or option +is restored at the end of the current module but it is *not* restored +at the end of the current section. Newly opened modules and sections inherit the current settings. .. note:: - We discourage using the :attr:`global` attribute with the :cmd:`Set` and - :cmd:`Unset` commands. If your goal is to define + We discourage using the :attr:`global` locality attribute with the + :cmd:`Set` and :cmd:`Unset` commands. If your goal is to define project-wide settings, you should rather use the command-line arguments ``-set`` and ``-unset`` for setting flags and options (see :ref:`command-line-options`). diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst index cf46580bdb..e742139134 100644 --- a/doc/sphinx/language/core/coinductive.rst +++ b/doc/sphinx/language/core/coinductive.rst @@ -194,7 +194,7 @@ Top-level definitions of co-recursive functions As in the :cmd:`Fixpoint` command, the :n:`with` clause allows simultaneously defining several mutual cofixpoints. - If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof 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 for which the computational behavior is relevant. See :ref:`proof-editing-mode`. diff --git a/doc/sphinx/language/core/conversion.rst b/doc/sphinx/language/core/conversion.rst index 7395b12339..09c619338b 100644 --- a/doc/sphinx/language/core/conversion.rst +++ b/doc/sphinx/language/core/conversion.rst @@ -47,7 +47,7 @@ refer the interested reader to :cite:`Coq85`. ι-reduction ~~~~~~~~~~~ -A specific conversion rule is associated to the inductive objects in +A specific conversion rule is associated with the inductive objects in the global environment. We shall give later on (see Section :ref:`Well-formed-inductive-definitions`) the precise rules but it just says that a destructor applied to an object built from a @@ -159,7 +159,8 @@ relation :math:`t` reduces to :math:`u` in the global environment reductions β, δ, ι or ζ. We say that two terms :math:`t_1` and :math:`t_2` are -*βδιζη-convertible*, or simply :gdef:`convertible`, or *equivalent*, in the +*βδιζη-convertible*, or simply :gdef:`convertible`, or +:term:`definitionally equal <definitional equality>`, in the global environment :math:`E` and local context :math:`Γ` iff there exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright … \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index ec5b896dab..7196c082ed 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -56,7 +56,7 @@ has type :n:`@type`. Top-level definitions --------------------- -Definitions extend the environment with associations of names to terms. +Definitions extend the global environment with associations of names to terms. A definition can be seen as a way to give a meaning to a name or as a way to abbreviate a term. In any case, the name can later be replaced at any time by its definition. @@ -82,7 +82,7 @@ Section :ref:`typing-rules`. | {* @binder } : @type reduce ::= Eval @red_expr in - These commands bind :n:`@term` to the name :n:`@ident` in the environment, + These commands bind :n:`@term` to the name :n:`@ident` in the global environment, provided that :n:`@term` is well-typed. They can take the :attr:`local` :term:`attribute`, which makes the defined :n:`@ident` accessible by :cmd:`Import` and its variants only through their fully qualified names. @@ -94,7 +94,7 @@ Section :ref:`typing-rules`. :attr:`bypass_check(universes)`, :attr:`bypass_check(guard)`, and :attr:`using` attributes. - If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof 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 for which the computational behavior is relevant. See :ref:`proof-editing-mode`. @@ -109,7 +109,7 @@ Section :ref:`typing-rules`. .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. .. exn:: @ident already exists. - :name: @ident already exists. (Definition) + :name: ‘ident’ already exists. (Definition) :undocumented: .. exn:: The term @term has type @type while it is expected to have type @type'. @@ -120,10 +120,11 @@ Section :ref:`typing-rules`. Assertions and proofs --------------------- -An assertion states a proposition (or a type) of which the proof (or an -inhabitant of the type) is interactively built using tactics. The interactive -proof mode is described in Chapter :ref:`proofhandling` and the tactics in -Chapter :ref:`Tactics`. The basic assertion command is: +An assertion states a proposition (or a type) for which the proof (or an +inhabitant of the type) is interactively built using :term:`tactics <tactic>`. +Assertions cause Coq to enter :term:`proof mode` (see :ref:`proofhandling`). +Common tactics are described in the :ref:`writing-proofs` chapter. +The basic assertion command is: .. cmd:: @thm_token @ident_decl {* @binder } : @type {* with @ident_decl {* @binder } : @type } :name: Theorem; Lemma; Fact; Remark; Corollary; Proposition; Property @@ -142,7 +143,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: After the statement is asserted, Coq needs a proof. Once a proof of :n:`@type` under the assumptions represented by :n:`@binder`\s is given and validated, the proof is generalized into a proof of :n:`forall {* @binder }, @type` and - the theorem is bound to the name :n:`@ident` in the environment. + the theorem is bound to the name :n:`@ident` in the global environment. These commands accept the :attr:`program` attribute. See :ref:`program_lemma`. @@ -159,7 +160,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: have to be used on *structurally smaller* arguments (for a :cmd:`Fixpoint`) or be *guarded by a constructor* (for a :cmd:`CoFixpoint`). The verification that recursive proof arguments are correct is done only at the time of registering - the lemma in the environment. To know if the use of induction hypotheses is + the lemma in the global environment. To know if the use of induction hypotheses is correct at some time of the interactive development of a proof, use the command :cmd:`Guarded`. @@ -170,7 +171,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: :undocumented: .. exn:: @ident already exists. - :name: @ident already exists. (Theorem) + :name: ‘ident’ already exists. (Theorem) The name you provided is already defined. You have then to choose another name. @@ -178,25 +179,24 @@ Chapter :ref:`Tactics`. The basic assertion command is: .. exn:: Nested proofs are discouraged and not allowed by default. This error probably means that you forgot to close the last "Proof." with "Qed." or "Defined.". \ If you really intended to use nested proofs, you can do so by turning the "Nested Proofs Allowed" flag on. - You are asserting a new statement while already being in proof editing mode. + You are asserting a new statement when you're already in proof mode. This feature, called nested proofs, is disabled by default. To activate it, turn the :flag:`Nested Proofs Allowed` flag on. -Proofs start with the keyword :cmd:`Proof`. Then Coq enters the proof editing mode -until the proof is completed. In proof editing mode, the user primarily enters -tactics, which are described in chapter :ref:`Tactics`. The user may also enter -commands to manage the proof editing mode. They are described in Chapter -:ref:`proofhandling`. +Proofs start with the keyword :cmd:`Proof`. Then Coq enters the proof mode +until the proof is completed. In proof mode, the user primarily enters +tactics (see :ref:`writing-proofs`). The user may also enter +commands to manage the proof mode (see :ref:`proofhandling`). When the proof is complete, use the :cmd:`Qed` command so the kernel verifies -the proof and adds it to the environment. +the proof and adds it to the global environment. .. note:: #. Several statements can be simultaneously asserted provided the :flag:`Nested Proofs Allowed` flag was turned on. - #. Not only other assertions but any vernacular command can be given + #. Not only other assertions but any command can be given while in the process of proving a given assertion. In this case, the command is understood as if it would have been given before the statements still to be proved. Nonetheless, this practice is discouraged @@ -211,4 +211,4 @@ the proof and adds it to the environment. side, :cmd:`Qed` (or :cmd:`Defined`) is mandatory to validate a proof. #. One can also use :cmd:`Admitted` in place of :cmd:`Qed` to turn the - current asserted statement into an axiom and exit the proof editing mode. + current asserted statement into an axiom and exit proof mode. diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 4bee7cc1b1..4e892f709d 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -36,7 +36,7 @@ Inductive types :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. + The :n:`@ident`\s are simultaneously added to the global environment before the types of constructors are checked. Each :n:`@ident` can be used independently thereafter. See :ref:`mutually_inductive_types`. @@ -86,7 +86,7 @@ A simple inductive type belongs to a universe that is a simple :n:`@sort`. The type nat is defined as the least :g:`Set` containing :g:`O` and closed by the :g:`S` constructor. The names :g:`nat`, :g:`O` and :g:`S` are added to the - environment. + global environment. This definition generates four elimination principles: :g:`nat_rect`, :g:`nat_ind`, :g:`nat_rec` and :g:`nat_sind`. The type of :g:`nat_ind` is: @@ -413,7 +413,7 @@ constructions. It is especially useful when defining functions over mutually defined inductive types. Example: :ref:`Mutual Fixpoints<example_mutual_fixpoints>`. - If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof 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 for which the computational behavior is relevant. See :ref:`proof-editing-mode`. @@ -636,7 +636,7 @@ contains an inductive definition. .. example:: - Provided that our environment :math:`E` contains inductive definitions we showed before, + Provided that our global environment :math:`E` contains inductive definitions we showed before, these two inference rules above enable us to conclude that: .. math:: diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index 6d96e15202..2e678c49d8 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -283,7 +283,6 @@ are now available through the dot notation. Check A.B.U. .. cmd:: Export {+ @filtered_import } - :name: Export Similar to :cmd:`Import`, except that when the module containing this command is imported, the :n:`{+ @qualid }` are imported as well. @@ -465,7 +464,7 @@ We also need additional typing judgments: + :math:`\WFT{E}{S}`, denoting that a structure :math:`S` is well-formed, + :math:`\WTM{E}{p}{S}`, denoting that the module pointed by :math:`p` has type :math:`S` in - environment :math:`E`. + the global environment :math:`E`. + :math:`\WEV{E}{S}{\ovl{S}}`, denoting that a structure :math:`S` is evaluated to a structure :math:`S` in weak head normal form. + :math:`\WS{E}{S_1}{S_2}` , denoting that a structure :math:`S_1` is a subtype of a @@ -881,7 +880,7 @@ started, unless option ``-top`` or ``-notop`` is set (see :ref:`command-line-opt .. _qualified-names: Qualified identifiers ---------------------- +~~~~~~~~~~~~~~~~~~~~~ .. insertprodn qualid field_ident @@ -965,7 +964,7 @@ names. A logical prefix Lib can be associated with a physical path using the command line option ``-Q`` `path` ``Lib``. All subfolders of path are -recursively associated to the logical path ``Lib`` extended with the +recursively associated with the logical path ``Lib`` extended with the corresponding suffix coming from the physical path. For instance, the folder ``path/fOO/Bar`` maps to ``Lib.fOO.Bar``. Subdirectories corresponding to invalid Coq identifiers are skipped, and, by convention, @@ -973,7 +972,7 @@ subdirectories named ``CVS`` or ``_darcs`` are skipped too. Thanks to this mechanism, ``.vo`` files are made available through the logical name of the folder they are in, extended with their own -basename. For example, the name associated to the file +basename. For example, the name associated with the file ``path/fOO/Bar/File.vo`` is ``Lib.fOO.Bar.File``. The same caveat applies for invalid identifiers. When compiling a source file, the ``.vo`` file stores its logical name, so that an error is issued if it is loaded with the @@ -1011,3 +1010,73 @@ subdirectories of path). See the command :cmd:`Declare ML Module` in See :ref:`command-line-options` for a more general view over the Coq command line options. + +.. _controlling-locality-of-commands: + +Controlling the scope of commands with locality attributes +---------------------------------------------------------- + +Many commands have effects that apply only within a specific scope, +typically the section or the module in which the command was +called. Locality :term:`attributes <attribute>` can alter the scope of +the effect. Below, we give the semantics of each locality attribute +while noting a few exceptional commands for which :attr:`local` and +:attr:`global` attributes are interpreted differently. + +.. attr:: local + + The :attr:`local` attribute limits the effect of the command to the + current scope (section or module). + + The ``Local`` prefix is an alternative syntax for the :attr:`local` + attribute (see :n:`@legacy_attr`). + + .. note:: + + - For some commands, this is the only locality supported within + sections (e.g., for :cmd:`Notation`, :cmd:`Ltac` and + :ref:`Hint <creating_hints>` commands). + + - For some commands, this is the default locality within + sections even though other locality attributes are supported + as well (e.g., for the :cmd:`Arguments` command). + + .. warning:: + + **Exception:** when :attr:`local` is applied to + :cmd:`Definition`, :cmd:`Theorem` or their variants, its + semantics are different: it makes the defined objects available + only through their fully-qualified names rather than their + unqualified names after an :cmd:`Import`. + +.. attr:: export + + The :attr:`export` attribute makes the effect of the command + persist when the section is closed and applies the effect when the + module containing the command is imported. + + Commands supporting this attribute include :cmd:`Set`, :cmd:`Unset` + and the :ref:`Hint <creating_hints>` commands, although the latter + don't support it within sections. + +.. attr:: global + + The :attr:`global` attribute makes the effect of the command + persist even when the current section or module is closed. Loading + the file containing the command (possibly transitively) applies the + effect of the command. + + The ``Global`` prefix is an alternative syntax for the + :attr:`global` attribute (see :n:`@legacy_attr`). + + .. warning:: + + **Exception:** for a few commands (like :cmd:`Notation` and + :cmd:`Ltac`), this attribute behaves like :attr:`export`. + + .. warning:: + + We strongly discourage using the :attr:`global` locality + attribute because the transitive nature of file loading gives + the user little control. We recommend using the :attr:`export` + locality attribute where it is supported. diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index 7eedbcd59a..6671c67fb2 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -119,13 +119,11 @@ The following settings let you control the display format for types: You can override the display format for specified types by adding entries to these tables: .. table:: Printing Record @qualid - :name: Printing Record Specifies a set of qualids which are displayed as records. Use the :cmd:`Add` and :cmd:`Remove` commands to update the set of qualids. .. table:: Printing Constructor @qualid - :name: Printing Constructor Specifies a set of qualids which are displayed as constructors. Use the :cmd:`Add` and :cmd:`Remove` commands to update the set of qualids. @@ -208,7 +206,7 @@ other arguments are the parameters of the inductive type. This message is followed by an explanation of this impossibility. There may be three reasons: - #. The name :token:`ident` already exists in the environment (see :cmd:`Axiom`). + #. The name :token:`ident` already exists in the global environment (see :cmd:`Axiom`). #. The body of :token:`ident` uses an incorrect elimination for :token:`ident` (see :cmd:`Fixpoint` and :ref:`Destructors`). #. The type of the projections :token:`ident` depends on previous diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst index 75389bb259..c16152ff4f 100644 --- a/doc/sphinx/language/core/sections.rst +++ b/doc/sphinx/language/core/sections.rst @@ -3,57 +3,33 @@ Section mechanism ----------------- -Sections create local contexts which can be shared across multiple definitions. - -.. example:: - - Sections are opened by the :cmd:`Section` command, and closed by :cmd:`End`. - - .. coqtop:: all - - Section s1. - - Inside a section, local parameters can be introduced using :cmd:`Variable`, - :cmd:`Hypothesis`, or :cmd:`Context` (there are also plural variants for - the first two). - - .. coqtop:: all - - Variables x y : nat. - - The command :cmd:`Let` introduces section-wide :ref:`let-in`. These definitions - won't persist when the section is closed, and all persistent definitions which - depend on `y'` will be prefixed with `let y' := y in`. - - .. coqtop:: in - - Let y' := y. - Definition x' := S x. - Definition x'' := x' + y'. - - .. coqtop:: all - - Print x'. - Print x''. - - End s1. - - Print x'. - Print x''. - - Notice the difference between the value of :g:`x'` and :g:`x''` inside section - :g:`s1` and outside. +Sections are naming scopes that permit creating section-local declarations that can +be used by other declarations in the section. Declarations made +with :cmd:`Variable`, :cmd:`Hypothesis`, :cmd:`Context`, +:cmd:`Let`, :cmd:`Let Fixpoint` and +:cmd:`Let CoFixpoint` (or the plural variants of the first two) within sections +are local to the section. + +In proofs done within the section, section-local declarations +are included in the :term:`local context` of the initial goal of the proof. +They are also accessible in definitions made with the :cmd:`Definition` command. + +Sections are opened by the :cmd:`Section` command, and closed by :cmd:`End`. +Sections can be nested. +When a section is closed, its local declarations are no longer available. +Global declarations that refer to them will be adjusted so they're still +usable outside the section as shown in this :ref:`example <section_local_declarations>`. .. cmd:: Section @ident - This command is used to open a section named :token:`ident`. + Opens the section named :token:`ident`. Section names do not need to be unique. .. cmd:: End @ident - This command closes the section or module named :token:`ident`. - See :ref:`Terminating an interactive module or module type definition<terminating_module>` + Closes the section or module named :token:`ident`. + See :ref:`Terminating an interactive module or module type definition <terminating_module>` for a description of its use with modules. After closing the @@ -78,14 +54,14 @@ Sections create local contexts which can be shared across multiple definitions. Let CoFixpoint @cofix_definition {* with @cofix_definition } :name: Let; Let Fixpoint; Let CoFixpoint - These commands behave like :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, except that + These are similar to :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, except that the declared constant is local to the current section. When the section is closed, all persistent definitions and theorems within it that depend on the constant will be wrapped with a :n:`@term_let` with the same declaration. As for :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, - if :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + if :n:`@term` is omitted, :n:`@type` is required and Coq enters proof 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 for which the computational behavior is relevant. See :ref:`proof-editing-mode`. @@ -103,3 +79,38 @@ Sections create local contexts which can be shared across multiple definitions. Context (b' := b). .. seealso:: Section :ref:`binders`. Section :ref:`contexts` in chapter :ref:`typeclasses`. + +.. _section_local_declarations: + +.. example:: Section-local declarations + + .. coqtop:: all + + Section s1. + + .. coqtop:: all + + Variables x y : nat. + + The command :cmd:`Let` introduces section-wide :ref:`let-in`. These definitions + won't persist when the section is closed, and all persistent definitions which + depend on `y'` will be prefixed with `let y' := y in`. + + .. coqtop:: in + + Let y' := y. + Definition x' := S x. + Definition x'' := x' + y'. + + .. coqtop:: all + + Print x'. + Print x''. + + End s1. + + Print x'. + Print x''. + + Notice the difference between the value of :g:`x'` and :g:`x''` inside section + :g:`s1` and outside. diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst index 95c5914e47..214541570c 100644 --- a/doc/sphinx/language/extensions/arguments-command.rst +++ b/doc/sphinx/language/extensions/arguments-command.rst @@ -4,7 +4,6 @@ Setting properties of a function's arguments ++++++++++++++++++++++++++++++++++++++++++++ .. cmd:: Arguments @reference {* @arg_specs } {* , {* @implicits_alt } } {? : {+, @args_modifier } } - :name: Arguments .. insertprodn argument_spec args_modifier @@ -79,7 +78,7 @@ Setting properties of a function's arguments `!` the function will be unfolded only if all the arguments marked with `!` - evaulate to constructors. See :ref:`Args_effect_on_unfolding`. + evaluate to constructors. See :ref:`Args_effect_on_unfolding`. :n:`@name {? % @scope }` a *formal parameter* of the function :n:`@reference` (i.e. diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index aa754ab63d..4cc35794cc 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -199,8 +199,8 @@ but also that the infix relation was bound to the ``nat_eq`` relation. This relation is selected whenever ``==`` is used on terms of type nat. This can be read in the line declaring the canonical structure ``nat_EQty``, where the first argument to ``Pack`` is the key and its second -argument a group of canonical values associated to the key. In this -case we associate to nat only one canonical value (since its class, +argument a group of canonical values associated with the key. In this +case we associate with nat only one canonical value (since its class, ``nat_EQcl`` has just one member). The use of the projection ``op`` requires its argument to be in the class ``EQ``, and uses such a member (function) to actually compare its arguments. @@ -530,7 +530,7 @@ instances of the ``LEQ`` class. The object ``Pack`` takes a type ``T`` (the key) and a mixin ``m``. It infers all the other pieces of the class ``LEQ`` and declares them as canonical -values associated to the ``T`` key. All in all, the only new piece of +values associated with the ``T`` key. All in all, the only new piece of information we add in the ``LEQ`` class is the mixin, all the rest is already canonical for ``T`` and hence can be inferred by Coq. diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst index fd9695e270..7206fb8581 100644 --- a/doc/sphinx/language/extensions/evars.rst +++ b/doc/sphinx/language/extensions/evars.rst @@ -5,6 +5,9 @@ Existential variables --------------------- +:gdef:`Existential variables <existential variable>` represent as yet unknown +values. + .. insertprodn term_evar term_evar .. prodn:: diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst index 23ba5f703a..765d04ec88 100644 --- a/doc/sphinx/language/extensions/implicit-arguments.rst +++ b/doc/sphinx/language/extensions/implicit-arguments.rst @@ -66,7 +66,7 @@ would be a solution of the inference problem. **Contextual Implicit Arguments** An implicit argument can be *contextual* or not. An implicit argument -is said *contextual* if it can be inferred only from the knowledge of +is said to be *contextual* if it can be inferred only from the knowledge of the type of the context of the current expression. For instance, the only argument of:: @@ -384,7 +384,7 @@ Displaying implicit arguments when pretty-printing .. flag:: Printing Implicit - By default, the basic pretty-printing rules hide the inferrable implicit + By default, the basic pretty-printing rules hide the inferable implicit arguments of an application. Turn this flag on to force printing all implicit arguments. @@ -506,7 +506,7 @@ or :g:`m` to the type :g:`nat` of natural numbers). .. flag:: Printing Use Implicit Types By default, the type of bound variables is not printed when - the variable name is associated to an implicit type which matches the + the variable name is associated with an implicit type which matches the actual type of the variable. This feature can be deactivated by turning this flag off. diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index 8e62c2af13..1c022448b0 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -252,7 +252,6 @@ If an inductive type has just one constructor, pattern matching can be written using the first destructuring let syntax. .. table:: Printing Let @qualid - :name: Printing Let Specifies a set of qualids for which pattern matching is displayed using a let expression. Note that this only applies to pattern matching instances entered with :g:`match`. @@ -269,7 +268,6 @@ can be written using ``if`` … ``then`` … ``else`` …. This table controls which types are written this way: .. table:: Printing If @qualid - :name: Printing If Specifies a set of qualids for which pattern matching is displayed using ``if`` … ``then`` … ``else`` …. Use the :cmd:`Add` and :cmd:`Remove` @@ -720,7 +718,7 @@ Recall that a list of patterns is also a pattern. So, when we destructure several terms at the same time and the branches have different types we need to provide the elimination predicate for this multiple pattern. It is done using the same scheme: each term may be -associated to an ``as`` clause and an ``in`` clause in order to introduce +associated with an ``as`` clause and an ``in`` clause in order to introduce a dependent product. For example, an equivalent definition for :g:`concat` (even though the diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index d20a82e6c0..a10312972e 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -43,7 +43,7 @@ Batch compilation (coqc) ------------------------ The ``coqc`` command takes a name *file* as argument. Then it looks for a -vernacular file named *file*.v, and tries to compile it into a +file named *file*.v, and tries to compile it into a *file*.vo file (See :ref:`compiled-files`). .. caution:: @@ -219,6 +219,71 @@ and ``coqtop``, unless stated otherwise: :-batch: Exit just after argument parsing. Available for ``coqtop`` only. :-verbose: Output the content of the input file as it is compiled. This option is available for ``coqc`` only. +:-native-compiler (yes|no|ondemand): Enable the :tacn:`native_compute` + reduction machine and precompilation to ``.cmxs`` files for future use + by :tacn:`native_compute`. + Setting ``yes`` enables :tacn:`native_compute`; it also causes Coq + to precompile the native code for future use; all dependencies need + to have been precompiled beforehand. Setting ``no`` disables + :tacn:`native_compute` which defaults back to :tacn:`vm_compute`; no files are precompiled. + Setting ``ondemand`` enables :tacn:`native_compute` + but disables precompilation; all missing dependencies will be recompiled + every time :tacn:`native_compute` is called. + + .. _native-compiler-options: + + .. versionchanged:: 8.13 + + The default value is set at configure time, + ``-config`` can be used to retrieve it. + All this can be summarized in the following table: + + .. list-table:: + :header-rows: 1 + + * - ``configure`` + - ``coqc`` + - ``native_compute`` + - outcome + - requirements + * - yes + - yes (default) + - native_compute + - ``.cmxs`` + - ``.cmxs`` of deps + * - yes + - no + - vm_compute + - none + - none + * - yes + - ondemand + - native_compute + - none + - none + * - no + - yes, no, ondemand + - vm_compute + - none + - none + * - ondemand + - yes + - native_compute + - ``.cmxs`` + - ``.cmxs`` of deps + * - ondemand + - no + - vm_compute + - none + - none + * - ondemand + - ondemand (default) + - native_compute + - none + - none + +:-native-output-dir: Set the directory in which to put the aforementioned + ``.cmxs`` for :tacn:`native_compute`. Defaults to ``.coq-native``. :-vos: Indicate Coq to skip the processing of opaque proofs (i.e., proofs ending with :cmd:`Qed` or :cmd:`Admitted`), output a ``.vos`` files instead of a ``.vo`` file, and to load ``.vos`` files instead of ``.vo`` files @@ -434,7 +499,7 @@ wrong. In the current version, it does not modify the compiled libraries to mark them as successfully checked. Note that non-logical information is not checked. By logical -information, we mean the type and optional body associated to names. +information, we mean the type and optional body associated with names. It excludes for instance anything related to the concrete syntax of objects (customized syntax rules, association between short and long names), implicit arguments, etc. diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index c239797cc2..dcc60195ed 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -7,7 +7,7 @@ Coq Integrated Development Environment The Coq Integrated Development Environment is a graphical tool, to be used as a user-friendly replacement to `coqtop`. Its main purpose is to -allow the user to navigate forward and backward into a Coq vernacular +allow the user to navigate forward and backward into a Coq file, executing corresponding commands or undoing them respectively. CoqIDE is run by typing the command `coqide` on the command line. @@ -100,10 +100,10 @@ processed color, though their preceding proofs have the processed color. Notice that for all these buttons, except for the "gears" button, their operations are also available in the menu, where their keyboard shortcuts are given. -Vernacular commands, templates ------------------------------------ +Commands and templates +---------------------- -The Templates menu allows using shortcuts to insert vernacular +The Templates menu allows using shortcuts to insert commands. This is a nice way to proceed if you are not sure of the syntax of the command you want. @@ -116,7 +116,7 @@ Queries .. image:: ../_static/coqide-queries.png :alt: CoqIDE queries -We call *query* any vernacular command that does not change the current state, +We call *query* any command that does not change the current state, such as ``Check``, ``Search``, etc. To run such commands interactively, without writing them in scripts, CoqIDE offers a *query pane*. The query pane can be displayed on demand by using the ``View`` menu, or using the shortcut ``F1``. diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index b63ae32311..2046788ef3 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -339,7 +339,7 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: in - Hint Rewrite Ack0 Ack1 Ack2 : base0. + Global Hint Rewrite Ack0 Ack1 Ack2 : base0. .. coqtop:: all @@ -367,7 +367,7 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: in - Hint Rewrite g0 g1 g2 using lia : base1. + Global Hint Rewrite g0 g1 g2 using lia : base1. .. coqtop:: in diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 87a367fc93..013ff0a83f 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -284,6 +284,8 @@ A sequence is an expression of the following form: .. tacn:: @ltac_expr3__1 ; {| @ltac_expr3__2 | @binder_tactic } :name: ltac-seq + .. todo: can't use "… ; …" as the name because of the semicolon + The expression :n:`@ltac_expr3__1` is evaluated to :n:`v__1`, which must be a tactic value. The tactic :n:`v__1` is applied to the current goals, possibly producing more goals. Then the right-hand side is evaluated to @@ -481,7 +483,6 @@ Do loop ~~~~~~~ .. tacn:: do @nat_or_var @ltac_expr3 - :name: do The do loop repeats a tactic :token:`nat_or_var` times: @@ -497,7 +498,6 @@ Repeat loop ~~~~~~~~~~~ .. tacn:: repeat @ltac_expr3 - :name: repeat The repeat loop repeats a tactic until it fails. @@ -515,7 +515,6 @@ Catching errors: try We can catch the tactic errors with: .. tacn:: try @ltac_expr3 - :name: try :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied to each focused goal independently. If the application of @@ -531,7 +530,6 @@ Detecting progress We can check if a tactic made progress with: .. tacn:: progress @ltac_expr3 - :name: progress :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied to each focused subgoal independently. If the application of ``v`` @@ -641,7 +639,6 @@ First tactic to succeed In some cases backtracking may be too expensive. .. tacn:: first [ {*| @ltac_expr } ] - :name: first For each focused goal, independently apply the first :token:`ltac_expr` that succeeds. The :n:`@ltac_expr`\s must evaluate to tactic values. @@ -701,7 +698,6 @@ Selects and applies the first tactic that solves each goal (i.e. leaves no subgo in a series of alternative tactics: .. tacn:: solve [ {*| @ltac_expr__i } ] - :name: solve For each current subgoal: evaluates and applies each :n:`@ltac_expr` in order until one is found that solves the subgoal. @@ -743,7 +739,6 @@ Conditional branching: tryif ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. tacn:: tryif @ltac_expr__test then @ltac_expr__then else @ltac_expr2__else - :name: tryif For each focused goal, independently: Evaluate and apply :n:`@ltac_expr__test`. If :n:`@ltac_expr__test` succeeds at least once, evaluate and apply :n:`@ltac_expr__then` @@ -772,7 +767,6 @@ Another way of restricting backtracking is to restrict a tactic to a single success: .. tacn:: once @ltac_expr3 - :name: once :n:`@ltac_expr3` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied but only its first success is used. If ``v`` fails, @@ -788,7 +782,6 @@ Coq provides an experimental way to check that a tactic has *exactly one* success: .. tacn:: exactly_once @ltac_expr3 - :name: exactly_once :n:`@ltac_expr3` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied if it has at most one success. If ``v`` fails, @@ -816,7 +809,6 @@ Checking for failure: assert_fails Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*: .. tacn:: assert_fails @ltac_expr3 - :name: assert_fails If :n:`@ltac_expr3` fails, the proof state is unchanged and no message is printed. If :n:`@ltac_expr3` unexpectedly has at least one success, the tactic performs @@ -863,7 +855,6 @@ Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic has *at le success: .. tacn:: assert_succeeds @ltac_expr3 - :name: assert_succeeds If :n:`@ltac_expr3` has at least one success, the proof state is unchanged and no message is printed. If :n:`@ltac_expr3` fails, the tactic performs @@ -877,7 +868,6 @@ Print/identity tactic: idtac .. tacn:: idtac {* {| @ident | @string | @natural } } - :name: idtac Leaves the proof unchanged and prints the given tokens. :token:`String<string>`\s and :token:`natural`\s are printed @@ -889,7 +879,7 @@ Print/identity tactic: idtac Failing ~~~~~~~ -.. tacn:: {| fail | gfail } {? @int_or_var } {* {| @ident | @string | @natural } } +.. tacn:: {| fail | gfail } {? @nat_or_var } {* {| @ident | @string | @natural } } :name: fail; gfail :tacn:`fail` is the always-failing tactic: it does not solve any @@ -910,7 +900,7 @@ Failing tactic into the goals, meaning that if there are no goals when it is evaluated, a tactic call like :tacn:`let` :n:`x := H in` :tacn:`fail` `0 x` will succeed. - :n:`@int_or_var` + :n:`@nat_or_var` The failure level. If no level is specified, it defaults to 0. The level is used by :tacn:`try`, :tacn:`repeat`, :tacn:`match goal` and the branching tacticals. If 0, it makes :tacn:`match goal` consider the next clause @@ -974,7 +964,6 @@ We can force a tactic to stop if it has not finished after a certain amount of time: .. tacn:: timeout @nat_or_var @ltac_expr3 - :name: timeout :n:`@ltac_expr3` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied normally, except that it is interrupted after :n:`@nat_or_var` seconds @@ -998,7 +987,6 @@ Timing a tactic A tactic execution can be timed: .. tacn:: time {? @string } @ltac_expr3 - :name: time evaluates :n:`@ltac_expr3` and displays the running time of the tactic expression, whether it fails or succeeds. In case of several successes, the time for each successive @@ -1015,7 +1003,6 @@ Tactic expressions that produce terms can be timed with the experimental tactic .. tacn:: time_constr @ltac_expr - :name: time_constr which evaluates :n:`@ltac_expr ()` and displays the time the tactic expression evaluated, assuming successful evaluation. Time is in seconds and is @@ -1026,12 +1013,10 @@ tactic implemented using the following internal tactics: .. tacn:: restart_timer {? @string } - :name: restart_timer Reset a timer .. tacn:: finish_timing {? ( @string ) } {? @string } - :name: finish_timing Display an optionally named timer. The parenthesized string argument is also optional, and determines the label associated with the timer @@ -1362,7 +1347,7 @@ Pattern matching on goals and hypotheses: match goal :tacn:`lazymatch goal`, :tacn:`match goal` and :tacn:`multimatch goal` are :token:`l1_tactic`\s. - Use this form to match hypotheses and/or goals in the proof context. These patterns have zero or + Use this form to match hypotheses and/or goals in the local context. These patterns have zero or more subpatterns to match hypotheses followed by a subpattern to match the conclusion. Except for the differences noted below, this works the same as the corresponding :n:`@match_key @ltac_expr` construct (see :tacn:`match`). Each current goal is processed independently. @@ -1533,7 +1518,7 @@ expression returns an identifier: .. todo you can't have a :tacn: with the same name as a :gdef: for now, eg `fresh` can't be both - Returns a fresh identifier name (i.e. one that is not already used in the context + Returns a fresh identifier name (i.e. one that is not already used in the local context and not previously returned by :tacn:`fresh` in the current :token:`ltac_expr`). The fresh identifier is formed by concatenating the final :token:`ident` of each :token:`qualid` (dropping any qualified components) and each specified :token:`string`. @@ -1541,11 +1526,11 @@ expression returns an identifier: If no arguments are given, the name is a fresh derivative of the name ``H``. .. note:: We recommend generating the fresh identifier immediately before - adding it in the proof context. Using :tacn:`fresh` in a local function + adding it to the local context. Using :tacn:`fresh` in a local function may not work as you expect: - Successive :tacn:`fresh`\es give distinct names even if the names haven't - yet been added to the proof context: + Successive calls to :tacn:`fresh` give distinct names even if the names haven't + yet been added to the local context: .. coqtop:: reset none @@ -1635,7 +1620,6 @@ Testing boolean expressions: guard ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. tacn:: guard @int_or_var @comparison @int_or_var - :name: guard .. insertprodn int_or_var comparison @@ -1734,7 +1718,6 @@ Defining |Ltac| symbols .. index:: ::= .. cmd:: Ltac @tacdef_body {* with @tacdef_body } - :name: Ltac .. insertprodn tacdef_body tacdef_body @@ -2248,7 +2231,6 @@ Tracing execution not printed. .. opt:: Info Level @natural - :name: Info Level This option is an alternative to the :cmd:`Info` command. @@ -2269,17 +2251,17 @@ The debugger stops, prompting for a command which can be one of the following: +-----------------+-----------------------------------------------+ -| simple newline: | go to the next step | +| newline | go to the next step | +-----------------+-----------------------------------------------+ -| h: | get help | +| h | get help | +-----------------+-----------------------------------------------+ -| x: | exit current evaluation | +| r n | advance n steps further | +-----------------+-----------------------------------------------+ -| s: | continue current evaluation without stopping | +| r string | advance up to the next call to “idtac string” | +-----------------+-----------------------------------------------+ -| r n: | advance n steps further | +| s | continue current evaluation without stopping | +-----------------+-----------------------------------------------+ -| r string: | advance up to the next call to “idtac string” | +| x | exit current evaluation | +-----------------+-----------------------------------------------+ .. exn:: Debug mode not available in the IDE @@ -2366,25 +2348,21 @@ performance issue. Unset Ltac Profiling. .. tacn:: start ltac profiling - :name: start ltac profiling This tactic behaves like :tacn:`idtac` but enables the profiler. .. tacn:: stop ltac profiling - :name: stop ltac profiling Similarly to :tacn:`start ltac profiling`, this tactic behaves like :tacn:`idtac`. Together, they allow you to exclude parts of a proof script from profiling. .. tacn:: reset ltac profile - :name: reset ltac profile Equivalent to the :cmd:`Reset Ltac Profile` command, which allows resetting the profile from tactic scripts for benchmarking purposes. .. tacn:: show ltac profile {? {| cutoff @integer | @string } } - :name: show ltac profile Equivalent to the :cmd:`Show Ltac Profile` command, which allows displaying the profile from tactic scripts for @@ -2410,11 +2388,10 @@ Run-time optimization tactic ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. tacn:: optimize_heap - :name: optimize_heap This tactic behaves like :tacn:`idtac`, except that running it compacts the - heap in the OCaml run-time system. It is analogous to the Vernacular - command :cmd:`Optimize Heap`. + heap in the OCaml run-time system. It is analogous to the + :cmd:`Optimize Heap` command. .. tacn:: infoH @ltac_expr3 diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 375129c02d..1bb4216e4f 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -173,7 +173,6 @@ Type declarations One can define new types with the following commands. .. cmd:: Ltac2 Type {? rec } @tac2typ_def {* with @tac2typ_def } - :name: Ltac2 Type .. insertprodn tac2typ_def tac2rec_field @@ -301,7 +300,6 @@ Ltac2 Definitions ~~~~~~~~~~~~~~~~~ .. cmd:: Ltac2 {? mutable } {? rec } @tac2def_body {* with @tac2def_body } - :name: Ltac2 .. insertprodn tac2def_body tac2def_body @@ -322,7 +320,6 @@ Ltac2 Definitions If ``mutable`` is set, the definition can be redefined at a later stage (see below). .. cmd:: Ltac2 Set @qualid {? as @ident } := @ltac2_expr - :name: Ltac2 Set This command redefines a previous ``mutable`` definition. Mutable definitions act like dynamic binding, i.e. at runtime, the last defined @@ -557,7 +554,7 @@ Built-in quotations ltac2_quotations ::= ident : ( @lident ) | constr : ( @term ) | open_constr : ( @term ) - | pattern : ( @cpattern ) + | pat : ( @cpattern ) | reference : ( {| & @ident | @qualid } ) | ltac1 : ( @ltac1_expr_in_env ) | ltac1val : ( @ltac1_expr_in_env ) @@ -571,7 +568,7 @@ The current implementation recognizes the following built-in quotations: (type ``Init.constr``). - ``open_constr``, which parses Coq terms and produces a term potentially with holes at runtime (type ``Init.constr`` as well). -- ``pattern``, which parses Coq patterns and produces a pattern used for term +- ``pat``, which parses Coq patterns and produces a pattern used for term matching (type ``Init.pattern``). - ``reference`` Qualified names are globalized at internalization into the corresponding global reference, @@ -598,7 +595,7 @@ modes, the *strict* and the *non-strict* mode. hypotheses. If this doesn't hold, internalization will fail. To work around this error, one has to specifically use the ``&`` notation. - In non-strict mode, any simple identifier appearing in a term quotation which - is not bound in the global context is turned into a dynamic reference to a + is not bound in the global environment is turned into a dynamic reference to a hypothesis. That is to say, internalization will succeed, but the evaluation of the term at runtime will fail if there is no such variable in the dynamic context. @@ -982,7 +979,7 @@ Match over goals gmatch_hyp_pattern ::= @name : @ltac2_match_pattern Matches over goals, similar to Ltac1 :tacn:`match goal`. - Use this form to match hypotheses and/or goals in the proof context. These patterns have zero or + Use this form to match hypotheses and/or goals in the local context. These patterns have zero or more subpatterns to match hypotheses followed by a subpattern to match the conclusion. Except for the differences noted below, this works the same as the corresponding :n:`@ltac2_match_key @ltac2_expr` construct (see :tacn:`match!`). Each current goal is processed independently. @@ -1164,7 +1161,6 @@ Notations --------- .. cmd:: Ltac2 Notation {+ @ltac2_scope } {? : @natural } := @ltac2_expr - :name: Ltac2 Notation .. todo seems like name maybe should use lident rather than ident, considering: @@ -1487,7 +1483,7 @@ Other nonterminals that have syntactic classes are listed here. * - :n:`conversion` - :token:`ltac2_conversion` - - :token:`conversion` + - * - :n:`rewriting` - :token:`ltac2_oriented_rewriter` @@ -1679,7 +1675,6 @@ Evaluation Ltac2 features a toplevel loop that can be used to evaluate expressions. .. cmd:: Ltac2 Eval @ltac2_expr - :name: Ltac2 Eval This command evaluates the term in the current proof if there is one, or in the global environment otherwise, and displays the resulting value to the user @@ -1877,9 +1872,9 @@ In Ltac expressions .. exn:: Unbound {| value | constructor } X - * if `X` is meant to be a term from the current stactic environment, replace + * if `X` is meant to be a term from the current static environment, replace the problematic use by `'X`. - * if `X` is meant to be a hypothesis from the goal context, replace the + * if `X` is meant to be a hypothesis from the local context, replace the problematic use by `&X`. In quotations @@ -1889,7 +1884,7 @@ In quotations * if `X` is meant to be a tactic expression bound by a Ltac2 let or function, replace the problematic use by `$X`. - * if `X` is meant to be a hypothesis from the goal context, replace the + * if `X` is meant to be a hypothesis from the local context, replace the problematic use by `&X`. Exception catching diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 07c2d268c6..bab9d35099 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -116,8 +116,8 @@ compatible with the rest of Coq, up to a few discrepancies: + New keywords (``is``) might clash with variable, constant, tactic or - tactical names, or with quasi-keywords in tactic or vernacular - notations. + tactical names, or with quasi-keywords in tactic or + notation commands. + New tactic(al)s names (:tacn:`last`, :tacn:`done`, :tacn:`have`, :tacn:`suffices`, :tacn:`suff`, :tacn:`without loss`, :tacn:`wlog`, :tacn:`congr`, :tacn:`unlock`) might clash with user tactic names. @@ -799,8 +799,9 @@ An *occurrence switch* can be: set x := {+1 3}(f 2). Notice that some occurrences of a given term may be - hidden to the user, for example because of a notation. The vernacular - ``Set Printing All`` command displays all these hidden occurrences and + hidden to the user, for example because of a notation. Setting the + :flag:`Printing All` flag causes these hidden occurrences to + be shown when the term is displayed. This setting should be used to find the correct coding of the occurrences to be selected [#1]_. @@ -1023,7 +1024,7 @@ conversely in between deductive steps. In |SSR| these moves are performed by two *tacticals* ``=>`` and ``:``, so that the bookkeeping required by a deductive step can be -directly associated to that step, and that tactics in an |SSR| +directly associated with that step, and that tactics in an |SSR| script correspond to actual logical steps in the proof rather than merely shuffle facts. Still, some isolated bookkeeping is unavoidable, such as naming variables and assumptions at the beginning of a @@ -1189,7 +1190,7 @@ The move tactic. ```````````````` .. tacn:: move - :name: move + :name: move (ssreflect) This tactic, in its defective form, behaves like the :tacn:`hnf` tactic. @@ -5502,7 +5503,7 @@ equivalences are indeed taken into account, otherwise only single string that contains symbols or is followed by a scope key, is interpreted as the constant whose notation involves that string (e.g., :g:`+` for :g:`addn`), if this is unambiguous; otherwise the diagnostic - includes the output of the :cmd:`Locate` vernacular command. + includes the output of the :cmd:`Locate` command. + whose statement, including assumptions and types, contains a subterm matching the next patterns. If a pattern is prefixed by ``-``, the test is reversed; diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 8f5c045929..665bae7077 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3,35 +3,46 @@ Tactics ======== -A deduction rule is a link between some (unique) formula, that we call -the *conclusion* and (several) formulas that we call the *premises*. A -deduction rule can be read in two ways. The first one says: “if I know -this and this then I can deduce this”. For instance, if I have a proof -of A and a proof of B then I have a proof of A ∧ B. This is forward -reasoning from premises to conclusion. The other way says: “to prove -this I have to prove this and this”. For instance, to prove A ∧ B, I -have to prove A and I have to prove B. This is backward reasoning from -conclusion to premises. We say that the conclusion is the *goal* to -prove and premises are the *subgoals*. The tactics implement *backward -reasoning*. When applied to a goal, a tactic replaces this goal with -the subgoals it generates. We say that a tactic reduces a goal to its -subgoal(s). - -Each (sub)goal is denoted with a number. The current goal is numbered -1. By default, a tactic is applied to the current goal, but one can -address a particular goal in the list by writing n:tactic which means -“apply tactic tactic to goal number n”. We can show the list of -subgoals by typing Show (see Section :ref:`requestinginformation`). - -Since not every rule applies to a given statement, not every tactic can -be used to reduce a given goal. In other words, before applying a tactic -to a given goal, the system checks that some *preconditions* are -satisfied. If it is not the case, the tactic raises an error message. - -Tactics are built from atomic tactics and tactic expressions (which -extends the folklore notion of tactical) to combine those atomic -tactics. This chapter is devoted to atomic tactics. The tactic -language will be described in Chapter :ref:`ltac`. +Tactics specify how to transform the :term:`proof state` of an +incomplete proof to eventually generate a complete proof. + +Proofs can be developed in two basic ways: In :gdef:`forward reasoning`, +the proof begins by proving simple statements that are then combined to prove the +theorem statement as the last step of the proof. With forward reasoning, +for example, +the proof of `A /\\ B` would begin with proofs of `A` and `B`, which are +then used to prove `A /\\ B`. Forward reasoning is probably the most common +approach in human-generated proofs. + +In :gdef:`backward reasoning`, the proof begins with the theorem statement +as the goal, which is then gradually transformed until every subgoal generated +along the way has been proven. In this case, the proof of `A /\\ B` begins +with that formula as the goal. This can be transformed into two subgoals, +`A` and `B`, followed by the proofs of `A` and `B`. Coq and its tactics +use backward reasoning. + +A tactic may fully prove a goal, in which case the goal is removed +from the proof state. +More commonly, a tactic replaces a goal with one or more :term:`subgoals <subgoal>`. +(We say that a tactic reduces a goal to its subgoals.) + +Most tactics require specific elements or preconditions to reduce a goal; +they display error messages if they can't be applied to the goal. +A few tactics, such as :tacn:`auto`, don't fail even if the proof state +is unchanged. + +Goals are identified by number. The current goal is number +1. Tactics are applied to the current goal by default. (The +default can be changed with the :opt:`Default Goal Selector` +option.) They can +be applied to another goal or to multiple goals with a +:ref:`goal selector <goal-selectors>` such as :n:`2: @tactic`. + +This chapter describes many of the most common built-in tactics. +Built-in tactics can be combined to form tactic expressions, which are +described in the :ref:`Ltac` chapter. Since tactic expressions can +be used anywhere that a built-in tactic can be used, "tactic" may +refer to both built-in tactics and tactic expressions. Common elements of tactics -------------------------- @@ -66,7 +77,7 @@ specified, the default selector is used. .. todo: fully describe selectors. At the moment, ltac has a fairly complete description .. todo: mention selectors can be applied to some commands, such as - Check, Search, SearchHead, SearchPattern, SearchRewrite. + Check, Search, SearchPattern, SearchRewrite. .. opt:: Default Goal Selector "@toplevel_selector" :name: Default Goal Selector @@ -264,17 +275,6 @@ These patterns can be used when the hypothesis is an equality: :n:`@simple_intropattern_closed`. :ref:`Example <intropattern_injection_ex>` -.. flag:: Bracketing Last Introduction Pattern - - For :n:`intros @intropattern_list`, controls how to handle a - conjunctive pattern that doesn't give enough simple patterns to match - all the arguments in the constructor. If set (the default), Coq generates - additional names to match the number of arguments. - Unsetting the flag will put the additional hypotheses in the goal instead, behavior that is more - similar to |SSR|'s intro patterns. - - .. deprecated:: 8.10 - .. _intropattern_cons_note: .. note:: @@ -498,10 +498,16 @@ one or more of its hypotheses. :n:`{? - } {+ @nat_or_var }` Selects the specified occurrences within a single goal or hypothesis. - Occurrences are numbered from left to right starting with 1 when the - goal is printed with the :flag:`Printing All` flag. (In particular, occurrences - in :ref:`implicit arguments <ImplicitArguments>` and - :ref:`coercions <Coercions>` are counted but not shown by default.) + Occurrences are numbered starting with 1 following a depth-first traversal + of the term's expression, including occurrences in + :ref:`implicit arguments <ImplicitArguments>` + and :ref:`coercions <Coercions>` that are not displayed by default. + (Set the :flag:`Printing All` flag to show those in the printed term.) + + For example, when matching the pattern `_ + _` in the term `(a + b) + c`, + occurrence 1 is `(...) + c` and + occurrence 2 is `(a + b)`. When matching that pattern with term `a + (b + c)`, + occurrence 1 is `a + (...)` and occurrence 2 is `b + c`. Specifying `-` includes all occurrences *except* the ones listed. @@ -540,8 +546,21 @@ one or more of its hypotheses. which is equivalent to `in * |- *`. Use `* |-` to select all occurrences in all hypotheses. -Tactics that use occurrence clauses include :tacn:`set`, -:tacn:`remember`, :tacn:`induction` and :tacn:`destruct`. + Tactics that select a specific hypothesis H to apply to other hypotheses, + such as :tacn:`rewrite` `H in * |-`, won't apply H to itself. + + If multiple + occurrences are given, such as in :tacn:`rewrite` `H at 1 2 3`, the tactic + must match at least one occurrence in order to succeed. The tactic will fail + if no occurrences match. Occurrence numbers that are out of range (e.g. + `at 1 3` when there are only 2 occurrences in the hypothesis or conclusion) + are ignored. + + .. todo: remove last sentence above and add "Invalid occurrence number @natural" exn for 8.14 + per #13568. + + Tactics that use occurrence clauses include :tacn:`set`, + :tacn:`remember`, :tacn:`induction` and :tacn:`destruct`. .. seealso:: @@ -1641,17 +1660,21 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. .. tacv:: instantiate (@natural := @term) - This variant allows to refer to an existential variable which was not named - by the user. The :n:`@natural` argument is the position of the existential variable - from right to left in the goal. Because this variant is not robust to slight - changes in the goal, its use is strongly discouraged. + This variant selects an existential variable by its position. The + :n:`@natural` argument is the position of the existential variable + *from right to left* in the conclusion of the goal. (Use one of + the variants below to select an existential variable in a + hypothesis.) Counting starts at 1 and multiple occurrences of the + same existential variable are counted multiple times. Because this + variant is not robust to slight changes in the goal, its use is + strongly discouraged. .. tacv:: instantiate ( @natural := @term ) in @ident instantiate ( @natural := @term ) in ( value of @ident ) instantiate ( @natural := @term ) in ( type of @ident ) These allow to refer respectively to existential variables occurring in a - hypothesis or in the body or the type of a local definition. + hypothesis or in the body or the type of a local definition (named :n:`@ident`). .. tacv:: instantiate @@ -1990,7 +2013,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) This is a more basic induction tactic. Again, the type of the argument :n:`@term` must be an inductive type. Then, according to the type of the goal, the tactic ``elim`` chooses the appropriate destructor and applies it - as the tactic :tacn:`apply` would do. For instance, if the proof context + as the tactic :tacn:`apply` would do. For instance, if the local context contains :g:`n:nat` and the current goal is :g:`T` of type :g:`Prop`, then :n:`elim n` is equivalent to :n:`apply nat_ind with (n:=n)`. The tactic ``elim`` does not modify the context of the goal, neither introduces the @@ -2050,19 +2073,6 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) is the name given by :n:`intros until @natural` to the :n:`@natural`-th non-dependent premise of the goal. -.. tacn:: double induction @ident @ident - :name: double induction - - This tactic is deprecated and should be replaced by - :n:`induction @ident; induction @ident` (or - :n:`induction @ident ; destruct @ident` depending on the exact needs). - -.. tacv:: double induction @natural__1 @natural__2 - - This tactic is deprecated and should be replaced by - :n:`induction num1; induction num3` where :n:`num3` is the result - of :n:`num2 - num1` - .. tacn:: dependent induction @ident :name: dependent induction @@ -2662,7 +2672,7 @@ and an explanation of the underlying technique. Like in a fix expression, the induction hypotheses have to be used on structurally smaller arguments. The verification that inductive proof arguments are correct is done only at the time of registering the - lemma in the environment. To know if the use of induction hypotheses + lemma in the global environment. To know if the use of induction hypotheses is correct at some time of the interactive development of a proof, use the command ``Guarded`` (see Section :ref:`requestinginformation`). @@ -2682,7 +2692,7 @@ and an explanation of the underlying technique. name given to the coinduction hypothesis. Like in a cofix expression, the use of induction hypotheses have to guarded by a constructor. The verification that the use of co-inductive hypotheses is correct is - done only at the time of registering the lemma in the environment. To + done only at the time of registering the lemma in the global environment. To know if the use of coinduction hypotheses is correct at some time of the interactive development of a proof, use the command ``Guarded`` (see Section :ref:`requestinginformation`). @@ -2763,14 +2773,11 @@ succeeds, and results in an error otherwise. :name: is_var This tactic checks whether its argument is a variable or hypothesis in - the current goal context or in the opened sections. + the current local context. .. exn:: Not a variable or hypothesis. :undocumented: - -.. _equality: - Equality -------- @@ -2965,59 +2972,7 @@ references to automatically generated names. Performance-oriented tactic variants ------------------------------------ -.. tacn:: change_no_check @term - :name: change_no_check - - For advanced usage. Similar to :tacn:`change` :n:`@term`, but as an optimization, - it skips checking that :n:`@term` is convertible to the goal. - - Recall that the Coq kernel typechecks proofs again when they are concluded to - ensure safety. Hence, using :tacn:`change` checks convertibility twice - overall, while :tacn:`change_no_check` can produce ill-typed terms, - but checks convertibility only once. - Hence, :tacn:`change_no_check` can be useful to speed up certain proof - scripts, especially if one knows by construction that the argument is - indeed convertible to the goal. - - In the following example, :tacn:`change_no_check` replaces :g:`False` by - :g:`True`, but :cmd:`Qed` then rejects the proof, ensuring consistency. - - .. example:: - - .. coqtop:: all abort - - Goal False. - change_no_check True. - exact I. - Fail Qed. - - :tacn:`change_no_check` supports all of :tacn:`change`'s variants. - - .. tacv:: change_no_check @term with @term’ - :undocumented: - - .. tacv:: change_no_check @term at {+ @natural} with @term’ - :undocumented: - - .. tacv:: change_no_check @term {? {? at {+ @natural}} with @term} in @ident - - .. example:: - - .. coqtop:: all abort - - Goal True -> False. - intro H. - change_no_check False in H. - exact H. - Fail Qed. - - .. tacv:: convert_concl_no_check @term - :name: convert_concl_no_check - - .. deprecated:: 8.11 - - Deprecated old name for :tacn:`change_no_check`. Does not support any of its - variants. +.. todo: move the following adjacent to the `exact` tactic in the rewriting chapter? .. tacn:: exact_no_check @term :name: exact_no_check diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index e866e4c624..8db16fff69 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1,7 +1,7 @@ .. _vernacularcommands: -Vernacular commands -============================= +Commands +======== .. _displaying: @@ -60,7 +60,7 @@ Query commands -------------- Unlike other commands, :production:`query_command`\s may be prefixed with -a goal selector (:n:`@natural:`) to specify which goal context it applies to. +a goal selector (:n:`@natural:`) to specify which goals it applies to. If no selector is provided, the command applies to the current goal. If no proof is open, then the command only applies to accessible objects. (see Section :ref:`invocation-of-tactics`). @@ -312,31 +312,6 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). Search is:Instance [ Reflexive | Symmetric ]. -.. cmd:: SearchHead @one_pattern {? {| inside | outside } {+ @qualid } } - - .. deprecated:: 8.12 - - Use the `headconcl:` clause of :cmd:`Search` instead. - - Displays the name and type of all hypotheses of the - selected goal (if any) and theorems of the current context that have the - form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_pattern` - matches a subterm of `C` in head position. For example, a :n:`@one_pattern` of `f _ b` - matches `f a b`, which is a subterm of `C` in head position when `C` is `f a b c`. - - See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. - - .. example:: :cmd:`SearchHead` examples - - .. coqtop:: none reset - - Add Search Blacklist "internal_". - - .. coqtop:: all warn - - SearchHead le. - SearchHead (@eq bool). - .. cmd:: SearchPattern @one_pattern {? {| inside | outside } {+ @qualid } } Displays the name and type of all hypotheses of the @@ -382,10 +357,9 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). SearchRewrite (_ + _ + _). .. table:: Search Blacklist @string - :name: Search Blacklist Specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`, - :cmd:`SearchHead`, :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries. A lemma whose + :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries. A lemma whose fully-qualified name contains any of the strings will be excluded from the search results. The default blacklisted substrings are ``_subterm``, ``_subproof`` and ``Private_``. @@ -396,7 +370,7 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). .. flag:: Search Output Name Only This flag restricts the output of search commands to identifier names; - turning it on causes invocations of :cmd:`Search`, :cmd:`SearchHead`, + turning it on causes invocations of :cmd:`Search`, :cmd:`SearchPattern`, :cmd:`SearchRewrite` etc. to omit types from their output, printing only identifiers. @@ -668,8 +642,8 @@ Loadpath ------------ Loadpaths are preferably managed using Coq command line options (see -Section :ref:`libraries-and-filesystem`) but there remain vernacular commands to manage them -for practical purposes. Such commands are only meant to be issued in +Section :ref:`libraries-and-filesystem`), but there are also commands +to manage them within Coq. These commands are only meant to be issued in the toplevel, and using them in source files is discouraged. @@ -740,7 +714,7 @@ Backtracking ------------ The backtracking commands described in this section can only be used -interactively, they cannot be part of a vernacular file loaded via +interactively, they cannot be part of a Coq file loaded via ``Load`` or compiled by ``coqc``. @@ -844,7 +818,6 @@ Quitting and debugging displayed. .. opt:: Default Timeout @natural - :name: Default Timeout If set, each :n:`@sentence` is treated as if it was prefixed with :cmd:`Timeout` :n:`@natural`, except for :cmd:`Timeout` commands themselves. If unset, @@ -883,7 +856,6 @@ Controlling display This flag controls the normal displaying. .. opt:: Warnings "{+, {? {| - | + } } @ident }" - :name: Warnings This option configures the display of warnings. It is experimental, and expects, between quotes, a comma-separated list of warning names or @@ -894,14 +866,12 @@ Controlling display right have higher priority, meaning that `A,-A` is equivalent to `-A`. .. opt:: Printing Width @natural - :name: Printing Width This command sets which left-aligned part of the width of the screen is used for display. At the time of writing this documentation, the default value is 78. .. opt:: Printing Depth @natural - :name: Printing Depth This option controls the nesting depth of the formatter used for pretty- printing. Beyond this depth, display of subterms is replaced by dots. At the @@ -1088,57 +1058,6 @@ described first. .. seealso:: :ref:`performingcomputations` -.. _controlling-locality-of-commands: - -Controlling the locality of commands ------------------------------------------ - -.. attr:: global - local - - Some commands support a :attr:`local` or :attr:`global` attribute - to control the scope of their effect. There is also a legacy (and - much more commonly used) syntax using the ``Local`` or ``Global`` - prefixes (see :n:`@legacy_attr`). There are four kinds of - commands: - - + Commands whose default is to extend their effect both outside the - section and the module or library file they occur in. For these - commands, the :attr:`local` attribute limits the effect of the command to the - current section or module it occurs in. As an example, the :cmd:`Coercion` - and :cmd:`Strategy` commands belong to this category. - + Commands whose default behavior is to stop their effect at the end - of the section they occur in but to extend their effect outside the module or - library file they occur in. For these commands, the :attr:`local` attribute limits the - effect of the command to the current module if the command does not occur in a - section and the :attr:`global` attribute extends the effect outside the current - sections and current module if the command occurs in a section. As an example, - the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong - to this category. Notice that a subclass of these commands do not support - extension of their scope outside sections at all and the :attr:`global` attribute is not - applicable to them. - + Commands whose default behavior is to stop their effect at the end - of the section or module they occur in. For these commands, the :attr:`global` - attribute extends their effect outside the sections and modules they - occur in. The :cmd:`Transparent` and :cmd:`Opaque` commands - belong to this category. - + Commands whose default behavior is to extend their effect outside - sections but not outside modules when they occur in a section and to - extend their effect outside the module or library file they occur in - when no section contains them. For these commands, the :attr:`local` attribute - limits the effect to the current section or module while the :attr:`global` - attribute extends the effect outside the module even when the command - occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this - category. - -.. attr:: export - - Some commands support an :attr:`export` attribute. The effect of - the attribute is to make the effect of the command available when - the module containing it is imported. It is supported in - particular by the :ref:`Hint <creating_hints>`, :cmd:`Set` and :cmd:`Unset` - commands. - .. _controlling-typing-flags: Controlling Typing Flags diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index 472df2bd91..30f7be5f13 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -273,18 +273,21 @@ Creating Hints :cmd:`Import` or :cmd:`Require` the current module. + :attr:`export` hints are visible from other modules when they :cmd:`Import` the current - module, but not when they only :cmd:`Require` it. This attribute is supported by - all `Hint` commands except for :cmd:`Hint Rewrite`. + module, but not when they only :cmd:`Require` it. + :attr:`global` hints are visible from other modules when they :cmd:`Import` or :cmd:`Require` the current module. + .. versionadded:: 8.14 + + The :cmd:`Hint Rewrite` now supports locality attributes like other `Hint` commands. + .. deprecated:: 8.13 The default value for hint locality will change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality will trigger a deprecation - warning. We recommend you use :attr:`export` whenever possible. + release. Hints added outside of sections without an explicit + locality are now deprecated. We recommend using :attr:`export` + where possible. The `Hint` commands are: @@ -335,7 +338,7 @@ Creating Hints .. exn:: @qualid cannot be used as a hint The head symbol of the type of :n:`@qualid` is a bound variable - such that this tactic cannot be associated to a constant. + such that this tactic cannot be associated with a constant. .. cmd:: Hint Immediate {+ {| @qualid | @one_term } } {? : {+ @ident } } diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst index 7724d7433c..63ddbd0a3a 100644 --- a/doc/sphinx/proofs/writing-proofs/index.rst +++ b/doc/sphinx/proofs/writing-proofs/index.rst @@ -10,19 +10,16 @@ the user and the assistant. The building blocks for this dialog are tactics which the user will use to represent steps in the proof of a theorem. -Incomplete proofs have one or more open (unproven) sub-goals. Each -goal has its own context (a set of assumptions that can be used to -prove the goal). Tactics can transform goals and contexts. -Internally, the incomplete proof is represented as a partial proof -term, with holes for the unproven sub-goals. +The first section presents the proof mode (the core mechanism of the +dialog between the user and the proof assistant). Then, several +sections describe the available tactics. One section covers the +SSReflect proof language, which provides a consistent alternative set +of tactics to the standard basic tactics. The last section documents +the ``Scheme`` family of commands, which can be used to extend the +power of the :tacn:`induction` and :tacn:`inversion` tactics. -When a proof is complete, the user leaves the proof mode and defers -the verification of the resulting proof term to the :ref:`kernel -<core-language>`. - -This chapter is divided in several parts, describing the basic ideas -of the proof mode (during which tactics can be used), and several -flavors of tactics, including the SSReflect proof language. +Additional tactics are documented in the next chapter +:ref:`automatic-tactics`. .. toctree:: :maxdepth: 1 diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst index 40d032543f..931ac905f6 100644 --- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst +++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst @@ -1,74 +1,175 @@ .. _proofhandling: -------------------- - Proof handling -------------------- +---------- +Proof mode +---------- -In Coq’s proof editing mode all top-level commands documented in -Chapter :ref:`vernacularcommands` remain available and the user has access to specialized -commands dealing with proof development pragmas documented in this -section. They can also use some other specialized commands called -*tactics*. They are the very tools allowing the user to deal with -logical reasoning. They are documented in Chapter :ref:`tactics`. +:gdef:`Proof mode <proof mode>` is used to prove theorems. +Coq enters proof mode when you begin a proof, +such as with the :cmd:`Theorem` command. It exits proof mode when +you complete a proof, such as with the :cmd:`Qed` command. Tactics, +which are available only in proof mode, incrementally transform incomplete +proofs to eventually generate a complete proof. -Coq user interfaces usually have a way of marking whether the user has -switched to proof editing mode. For instance, in coqtop the prompt ``Coq <`` is changed into -:n:`@ident <` where :token:`ident` is the declared name of the theorem currently edited. +When you run Coq interactively, such as through CoqIDE, Proof General or +coqtop, Coq shows the current proof state (the incomplete proof) as you +enter tactics. This information isn't shown when you run Coq in batch +mode with `coqc`. -At each stage of a proof development, one has a list of goals to -prove. Initially, the list consists only in the theorem itself. After -having applied some tactics, the list of goals contains the subgoals -generated by the tactics. +Proof State +----------- -To each subgoal is associated a number of hypotheses called the *local context* -of the goal. Initially, the local context contains the local variables and -hypotheses of the current section (see Section :ref:`gallina-assumptions`) and -the local variables and hypotheses of the theorem statement. It is enriched by -the use of certain tactics (see e.g. :tacn:`intro`). +The :gdef:`proof state` consists of one or more unproven goals. +Each goal has a :gdef:`conclusion` (the statement that is to be proven) +and a :gdef:`local context`, which contains named :term:`hypotheses <hypothesis>` +(which are propositions), variables and local definitions that can be used in +proving the conclusion. The proof may also use *constants* from the :term:`global environment` +such as definitions and proven theorems. -When a proof is completed, the message ``Proof completed`` is displayed. -One can then register this proof as a defined constant in the -environment. Because there exists a correspondence between proofs and -terms of λ-calculus, known as the *Curry-Howard isomorphism* -:cite:`How80,Bar81,Gir89,H89`, Coq stores proofs as terms of |Cic|. Those -terms are called *proof terms*. +The term ":gdef:`goal`" may refer to an entire goal or to the conclusion +of a goal, depending on the context. +The conclusion appears below a line and the local context appears above the line. +The conclusion is a type. Each item in the local context begins with a name +and ends, after a colon, with an associated type. +Local definitions are shown in the form `n := 0 : nat`, for example, in which `nat` is the +type of `0`. -.. exn:: No focused proof. +The local context of a goal contains items specific to the goal as well +as section-local variables and hypotheses (see :ref:`gallina-assumptions`) defined +in the current :ref:`section <section-mechanism>`. The latter are included in the +initial proof state. +Items in the local context are ordered; an item can only refer to items that appear +before it. (A more mathematical description of the *local context* is +:ref:`here <Local-context>`.) - Coq raises this error message when one attempts to use a proof editing command - out of the proof editing mode. +The :gdef:`global environment` has definitions and proven theorems that are global in scope. +(A more mathematical description of the *global environment* is :ref:`here <Global-environment>`.) + +When you begin proving a theorem, the proof state shows +the statement of the theorem below the line and often nothing in the +local context: + +.. coqtop:: none + + Parameter P: nat -> Prop. + +.. coqtop:: out + + Goal forall n m: nat, n > m -> P 1 /\ P 2. + +After applying the :tacn:`intros` :term:`tactic`, we see hypotheses above the line. +The names of variables (`n` and `m`) and hypotheses (`H`) appear before a colon, followed by +the type they represent. + +.. coqtop:: all + + intros. + +Some tactics, such as :tacn:`split`, create new goals, which may +be referred to as :gdef:`subgoals <subgoal>` for clarity. +Goals are numbered from 1 to N at each step of the proof to permit applying a +tactic to specific goals. The local context is only shown for the first goal. + +.. coqtop:: all + + split. + +"Variables" may refer specifically to local context items for which the type of their type +is `Set` or `Type`, and :gdef:`"hypotheses" <hypothesis>` refers to items that are +:term:`propositions <proposition>`, +for which the type of their type is `Prop` or `SProp`, +but these terms are also used interchangeably. + +.. coqtop:: out + + let t_n := type of n in idtac "type of n :" t_n; + let tt_n := type of t_n in idtac "type of" t_n ":" tt_n. + let t_H := type of H in idtac "type of H :" t_H; + let tt_H := type of t_H in idtac "type of" t_H ":" tt_H. + +A proof script, consisting of the tactics that are applied to prove a +theorem, is often informally referred to as a "proof". +The real proof, whether complete or incomplete, is a term, the :gdef:`proof term`, +which users may occasionally want to examine. (This is based on the +*Curry-Howard isomorphism* :cite:`How80,Bar81,Gir89,H89`, which is +a correspondence between between proofs and terms and between +propositions and types of λ-calculus. The isomorphism is also +sometimes called the "propositions-as-types correspondence".) + +The :cmd:`Show Proof` command displays the incomplete proof term +before you've completed the proof. For example, here's the proof +term after using the :tacn:`split` tactic above: + +.. coqtop:: all + + Show Proof. + +The incomplete parts, the goals, are represented by +:term:`existential variables <existential variable>` +with names that begin with `?Goal`. The :cmd:`Show Existentials` command +shows each existential with the hypotheses and conclusion for the associated goal. + +.. coqtop:: all + + Show Existentials. + +Coq's kernel verifies the correctness of proof terms when it exits +proof mode by checking that the proof term is :term:`well-typed` and +that its type is the same as the theorem statement. + +After a proof is completed, :cmd:`Print` `<theorem_name>` +shows the proof term and its type. The type appears after +the colon (`forall ...`), as for this theorem from Coq's standard library: + +.. coqtop:: all + + Print proj1. .. _proof-editing-mode: -Entering and leaving proof editing mode ---------------------------------------- +Entering and exiting proof mode +------------------------------- + +Coq enters :term:`proof mode` when you begin a proof through +commands such as :cmd:`Theorem` or :cmd:`Goal`. Coq user interfaces +usually have a way to indicate that you're in proof mode. + +:term:`Tactics <tactic>` are available only in proof mode (currently they give syntax +errors outside of proof mode). Most :term:`commands <command>` can be used both in and out of +proof mode, but some commands only work in or outside of proof mode. -The proof editing mode is entered by asserting a statement, which typically is -the assertion of a theorem using an assertion command like :cmd:`Theorem`. The -list of assertion commands is given in :ref:`Assertions`. The command -:cmd:`Goal` can also be used. +When the proof is completed, you can exit proof mode with commands such as +:cmd:`Qed`, :cmd:`Defined` and :cmd:`Save`. .. cmd:: Goal @type - This is intended for quick assertion of statements, without knowing in - advance which name to give to the assertion, typically for quick - testing of the provability of a statement. If the proof of the - statement is eventually completed and validated, the statement is then - bound to the name ``Unnamed_thm`` (or a variant of this name not already - used for another statement). + Asserts an unnamed proposition. This is intended for quick tests that + a proposition is provable. If the proof is eventually completed and + validated, you can assign a name with the :cmd:`Save` or :cmd:`Defined` + commands. If no name is given, the name will be `Unnamed_thm` (or, + if that name is already defined, a variant of that). .. cmd:: Qed - This command is available in interactive editing proof mode when the - proof is completed. Then :cmd:`Qed` extracts a proof term from the proof - script, switches back to Coq top-level and attaches the extracted - proof term to the declared name of the original goal. The name is - added to the environment as an opaque constant. + Passes a completed :term:`proof term` to Coq's kernel + to check that the proof term is :term:`well-typed` and + to verify that its type matches the theorem statement. If it's verified, the + proof term is added to the global environment as an opaque constant + using the declared name from the original goal. + + It's very rare for a proof term to fail verification. Generally this + indicates a bug in a tactic you used or that you misused some + unsafe tactics. .. exn:: Attempt to save an incomplete proof. :undocumented: + .. exn:: No focused proof (No proof-editing in progress). + + You tried to use a proof mode command such as :cmd:`Qed` outside of proof + mode. + .. note:: Sometimes an error occurs when building the proof term, because @@ -81,9 +182,9 @@ list of assertion commands is given in :ref:`Assertions`. The command even incur a memory overflow. .. cmd:: Save @ident - :name: Save - Saves a completed proof with the name :token:`ident`, which + Similar to :cmd:`Qed`, except that the proof term is added to the global + context with the name :token:`ident`, which overrides any name provided by the :cmd:`Theorem` command or its variants. @@ -98,7 +199,7 @@ list of assertion commands is given in :ref:`Assertions`. The command .. cmd:: Admitted - This command is available in interactive editing mode to give up + This command is available in proof mode to give up the current proof and declare the initial goal as an axiom. .. cmd:: Abort {? {| All | @ident } } @@ -120,7 +221,7 @@ list of assertion commands is given in :ref:`Assertions`. The command .. cmd:: Proof @term :name: Proof `term` - This command applies in proof editing mode. It is equivalent to + This command applies in proof mode. It is equivalent to :n:`exact @term. Qed.` That is, you have to give the full proof in one gulp, as a proof term (see Section :ref:`applyingtheorems`). @@ -159,7 +260,7 @@ list of assertion commands is given in :ref:`Assertions`. The command | Type {? * } | All - Opens proof editing mode, declaring the set of + Opens proof mode, declaring the set of section variables (see :ref:`gallina-assumptions`) used by the proof. At :cmd:`Qed` time, the system verifies that the set of section variables used in @@ -210,7 +311,7 @@ list of assertion commands is given in :ref:`Assertions`. The command .. example:: - .. coqtop:: all + .. coqtop:: all reset Section Test. Variable n : nat. @@ -232,7 +333,6 @@ The following options modify the behavior of ``Proof using``. .. opt:: Default Proof Using "@section_var_expr" - :name: Default Proof Using Use :n:`@section_var_expr` as the default ``Proof using`` value. E.g. ``Set Default Proof Using "a b"`` will complete all ``Proof`` commands not followed by a @@ -301,7 +401,7 @@ Name a set of section hypotheses for ``Proof using`` Use :cmd:`Unshelve` instead. Proof modes -``````````` +----------- When entering proof mode through commands such as :cmd:`Goal` and :cmd:`Proof`, Coq picks by default the |Ltac| mode. Nonetheless, there exist other proof modes @@ -312,8 +412,8 @@ be changed using the following option. .. opt:: Default Proof Mode @string Select the proof mode to use when starting a proof. Depending on the proof - mode, various syntactic constructs are allowed when writing an interactive - proof. All proof modes support vernacular commands; the proof mode determines + mode, various syntactic constructs are allowed when writing a + proof. All proof modes support commands; the proof mode determines which tactic language and set of tactic definitions are available. The possible option values are: @@ -349,16 +449,16 @@ Navigation in the proof tree .. cmd:: Restart - Restores the proof editing process to the original goal. + Restores the proof to the original goal. .. exn:: No focused proof to restart. :undocumented: .. cmd:: Focus {? @natural } - Focuses the attention on the first subgoal to prove or, if :token:`natural` is + Focuses the attention on the first goal to prove or, if :token:`natural` is specified, the :token:`natural`\-th. The - printing of the other subgoals is suspended until the focused subgoal + printing of the other goals is suspended until the focused goal is solved or unfocused. .. deprecated:: 8.8 @@ -379,14 +479,9 @@ Navigation in the proof tree .. _curly-braces: -.. index:: { - } - -.. todo: :name: "{"; "}" doesn't work, nor does :name: left curly bracket; right curly bracket, - hence the verbose names - .. tacn:: {? {| @natural | [ @ident ] } : } %{ - %} + %} + :name: {; } .. todo See https://github.com/coq/coq/issues/12004 and @@ -403,7 +498,7 @@ Navigation in the proof tree or focus the next one. :n:`@natural:` - Focuses on the :token:`natural`\-th subgoal to prove. + Focuses on the :token:`natural`\-th goal to prove. :n:`[ @ident ]: %{` Focuses on the named goal :token:`ident`. @@ -477,7 +572,7 @@ Navigation in the proof tree Brackets are used to focus on a single goal given either by its position or by its name if it has one. - .. seealso:: The error messages for bullets below. + .. seealso:: The error messages for bullets below. .. _bullets: @@ -567,7 +662,6 @@ Set Bullet Behavior ~~~~~~~~~~~~~~~~~~~ .. opt:: Bullet Behavior {| "None" | "Strict Subproofs" } - :name: Bullet Behavior This option controls the bullet behavior and can take two possible values: @@ -577,8 +671,7 @@ Set Bullet Behavior Modifying the order of goals ```````````````````````````` -.. tacn:: cycle @integer - :name: cycle +.. tacn:: cycle @int_or_var Reorders the selected goals so that the first :n:`@integer` goals appear after the other selected goals. @@ -601,8 +694,7 @@ Modifying the order of goals all: cycle 2. all: cycle -3. -.. tacn:: swap @integer @integer - :name: swap +.. tacn:: swap @int_or_var @int_or_var Exchanges the position of the specified goals. Negative values for :n:`@integer` indicate counting goals @@ -621,7 +713,6 @@ Modifying the order of goals all: swap 1 -1. .. tacn:: revgoals - :name: revgoals Reverses the order of the selected goals. The tactic is only useful with a goal selector, most commonly `all :`. Note that other selectors reorder goals; @@ -638,16 +729,17 @@ Modifying the order of goals Postponing the proof of some goals `````````````````````````````````` +Goals can be :gdef:`shelved` so they are no longer displayed in the proof state. +They can then be :gdef:`unshelved` to make them visible again. + .. tacn:: shelve - :name: shelve This tactic moves all goals under focus to a shelf. While on the shelf, goals will not be focused on. They can be solved by unification, or they can be called back into focus with the command :cmd:`Unshelve`. - .. tacv:: shelve_unifiable - :name: shelve_unifiable + .. tacn:: shelve_unifiable Shelves only the goals under focus that are mentioned in other goals. Goals that appear in the type of other goals can be solved by unification. @@ -667,14 +759,12 @@ Postponing the proof of some goals from the shelf into focus, by appending them to the end of the current list of focused goals. -.. tacn:: unshelve @tactic - :name: unshelve +.. tacn:: unshelve @ltac_expr1 Performs :n:`@tactic`, then unshelves existential variables added to the shelf by the execution of :n:`@tactic`, prepending them to the current goal. .. tacn:: give_up - :name: give_up This tactic removes the focused goals from the proof. They are not solved, and cannot be solved later in the proof. As the goals are not @@ -694,7 +784,7 @@ Requesting information Displays the current goals. :n:`@natural` - Display only the :token:`natural`\-th subgoal. + Display only the :token:`natural`\-th goal. :n:`@ident` Displays the named goal :token:`ident`. This is useful in @@ -791,7 +881,7 @@ Requesting information Some tactics (e.g. :tacn:`refine`) allow to build proofs using fixpoint or co-fixpoint constructions. Due to the incremental nature - of interactive proof construction, the check of the termination (or + of proof construction, the check of the termination (or guardedness) of the recursive calls in the fixpoint or cofixpoint constructions is postponed to the time of the completion of the proof. @@ -854,7 +944,6 @@ How to enable diffs ``````````````````` .. opt:: Diffs {| "on" | "off" | "removed" } - :name: Diffs The “on” setting highlights added tokens in green, while the “removed” setting additionally reprints items with removed tokens in red. Unchanged tokens in @@ -983,12 +1072,11 @@ To show differences in the proof term: .. image:: ../../_static/diffs-show-proof.png :alt: coqide with Set Diffs on with compacted hypotheses -Controlling the effect of proof editing commands ------------------------------------------------- +Controlling proof mode +---------------------- .. opt:: Hyps Limit @natural - :name: Hyps Limit This option controls the maximum number of hypotheses displayed in goals after the application of a tactic. All the hypotheses remain usable @@ -1009,7 +1097,7 @@ Controlling the effect of proof editing commands .. flag:: Printing Goal Names - When turned on, the name of the goal is printed in interactive + When turned on, the name of the goal is printed in proof mode, which can be useful in cases of cross references between goals. diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index b7f2927000..f286533d78 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -1,301 +1,388 @@ -================================= -Term rewriting and simplification -================================= +========================= +Reasoning with equalities +========================= + +There are multiple notions of :gdef:`equality` in Coq: + +- :gdef:`Leibniz equality` is the standard + way to define equality in Coq and the Calculus of Inductive Constructions, + which is in terms of a binary relation, i.e. a binary function that returns + a `Prop`. The standard library + defines `eq` similar to this: + + .. coqdoc:: + + Inductive eq {A : Type} (x : A) : A -> Prop := eq_refl : eq x x. + + The notation `x = y` represents the term `eq x y`. The notation `x = y :> A` + gives the type of x and y explicitly. + +- :gdef:`Setoid equality <setoid equality>` defines equality in terms of an equivalence + relation. A :gdef:`setoid` is a set that is equipped with an equivalence relation + (see https://en.wikipedia.org/wiki/Setoid). These are needed to form a :gdef:`quotient set` + or :gdef:`quotient` + (see https://en.wikipedia.org/wiki/Equivalence_Class). In Coq, users generally work + with setoids rather than constructing quotients, for which there is no specific support. + +- :gdef:`Definitional equality <definitional equality>` is equality based on the + :ref:`conversion rules <Conversion-rules>`, which Coq can determine automatically. + When two terms are definitionally equal, Coq knows it can + replace one with the other, such as with :tacn:`change` `X with Y`, among many + other advantages. ":term:`Convertible <convertible>`" is another way of saying that + two terms are definitionally equal. .. _rewritingexpressions: -Rewriting expressions ---------------------- +Rewriting with Leibniz and setoid equality +------------------------------------------ -These tactics use the equality :g:`eq:forall A:Type, A->A->Prop` defined in -file ``Logic.v`` (see :ref:`coq-library-logic`). The notation for :g:`eq T t u` is -simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. +.. tacn:: rewrite {+, @oriented_rewriter } {? @occurrences } {? by @ltac_expr3 } -.. tacn:: rewrite @term - :name: rewrite + .. insertprodn oriented_rewriter one_term_with_bindings - This tactic applies to any goal. The type of :token:`term` must have the form + .. prodn:: + oriented_rewriter ::= {? {| -> | <- } } {? @natural } {? {| ? | ! } } @one_term_with_bindings + one_term_with_bindings ::= {? > } @one_term {? with @bindings } - ``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``), eq term``:sub:`1` ``term``:sub:`2` ``.`` + Replaces subterms with other subterms that have been proven to be equal. + The type of :n:`@one_term` must have the form: - where :g:`eq` is the Leibniz equality or a registered setoid equality. + :n:`{? forall {+ (x__i: A__i) } , } EQ @term__1 @term__2` - Then :n:`rewrite @term` finds the first subterm matching `term`\ :sub:`1` in the goal, - resulting in instances `term`:sub:`1`' and `term`:sub:`2`' and then - replaces every occurrence of `term`:subscript:`1`' by `term`:subscript:`2`'. - Hence, some of the variables :g:`x`\ :sub:`i` are solved by unification, - and some of the types :g:`A`\ :sub:`1`:g:`, ..., A`\ :sub:`n` become new - subgoals. + .. todo :term:`Leibniz equality` does not work with Sphinx 2.3.1. It does with Sphinx 3.0.3. - .. exn:: The @term provided does not end with an equation. - :undocumented: + where :g:`EQ` is the Leibniz equality `eq` or a registered :term:`setoid equality`. + Note that :n:`eq @term__1 @term__2` is typically written with the infix notation + :n:`@term__1 = @term__2`. You must `Require Setoid` to use the tactic + with a setoid equality or with :ref:`setoid rewriting <generalizedrewriting>`. + In the general form, any :n:`@binder` may be used, not just :n:`(x__i: A__i)`. - .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal. - :undocumented: + .. todo doublecheck the @binder comment is correct. - .. tacv:: rewrite -> @term + :n:`rewrite @one_term` finds subterms matching :n:`@term__1` in the goal, + and replaces them with :n:`@term__2` (or the reverse if `<-` is given). + Some of the variables :g:`x`\ :sub:`i` are solved by unification, + and some of the types :n:`A__1, ..., A__n` may become new + subgoals. :tacn:`rewrite` won't find occurrences inside `forall` that refer + to variables bound by the `forall`; use the more advanced :tacn:`setoid_rewrite` + if you want to find such occurrences. - Is equivalent to :n:`rewrite @term` + :n:`{+, @oriented_rewriter }` + The :n:`@oriented_rewriter`\s are applied sequentially + to the first goal generated by the previous :n:`@oriented_rewriter`. If any of them fail, + the tactic fails. - .. tacv:: rewrite <- @term + :n:`{? {| -> | <- } }` + For `->` (the default), :n:`@term__1` is rewritten + into :n:`@term__2`. For `<-`, :n:`@term__2` is rewritten into :n:`@term__1`. - Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left + :n:`{? @natural } {? {| ? | ! } }` + :n:`@natural` is the number of rewrites to perform. If `?` is given, :n:`@natural` + is the maximum number of rewrites to perform; otherwise :n:`@natural` is the exact number + of rewrites to perform. - .. tacv:: rewrite @term in @goal_occurrences + `?` (without :n:`@natural`) performs the rewrite as many times as possible + (possibly zero times). + This form never fails. `!` (without :n:`@natural`) performs the rewrite as many + times as possible + and at least once. The tactic fails if the requested number of rewrites can't + be performed. :n:`@natural !` is equivalent to :n:`@natural`. - Analogous to :n:`rewrite @term` but rewriting is done following - the clause :token:`goal_occurrences`. For instance: + :n:`@occurrences` + If :n:`@occurrences` specifies multiple occurrences, the tactic succeeds if + any of them can be rewritten. If not specified, only the first occurrence + in the conclusion is replaced. - + :n:`rewrite H in H'` will rewrite `H` in the hypothesis - ``H'`` instead of the current goal. - + :n:`rewrite H in H' at 1, H'' at - 2 |- *` means - :n:`rewrite H; rewrite H in H' at 1; rewrite H in H'' at - 2.` - In particular a failure will happen if any of these three simpler tactics - fails. - + :n:`rewrite H in * |-` will do :n:`rewrite H in H'` for all hypotheses - :g:`H'` different from :g:`H`. - A success will happen as soon as at least one of these simpler tactics succeeds. - + :n:`rewrite H in *` is a combination of :n:`rewrite H` and :n:`rewrite H in * |-` - that succeeds if at least one of these two tactics succeeds. + .. note:: - Orientation :g:`->` or :g:`<-` can be inserted before the :token:`term` to rewrite. + If :n:`at @occs_nums` is specified, rewriting is always done + with :ref:`setoid rewriting <generalizedrewriting>`, even for + Leibniz equality, which means that you must `Require + Setoid` to use that form. However, note that :tacn:`rewrite` + (even when using setoid rewriting) and :tacn:`setoid_rewrite` + don't behave identically (as is noted above and below). - .. tacv:: rewrite @term at @occurrences + :n:`by @ltac_expr3` + If specified, is used to resolve all side conditions generated by the tactic. - Rewrite only the given :token:`occurrences` of :token:`term`. Occurrences are - specified from left to right as for pattern (:tacn:`pattern`). The rewrite is - always performed using setoid rewriting, even for Leibniz’s equality, so one - has to ``Import Setoid`` to use this variant. + .. note:: - .. tacv:: rewrite @term by @tactic + For each selected hypothesis and/or the conclusion, + :tacn:`rewrite` finds the first matching subterm in + depth-first search order. Only subterms identical to + that first matched subterm are rewritten. If the `at` clause is specified, + only these subterms are considered when counting occurrences. + To select a different set of matching subterms, you can + specify how some or all of the free variables are bound by + using a `with` clause (see :n:`@one_term_with_bindings`). - Use tactic to completely solve the side-conditions arising from the - :tacn:`rewrite`. + For instance, if we want to rewrite the right-hand side in the + following goal, this will not work: - .. tacv:: rewrite {+, @orientation @term} {? in @ident } + .. coqtop:: none - Is equivalent to the `n` successive tactics :n:`{+; rewrite @term}`, each one - working on the first subgoal generated by the previous one. An :production:`orientation` - ``->`` or ``<-`` can be inserted before each :token:`term` to rewrite. One - unique clause can be added at the end after the keyword in; it will then - affect all rewrite operations. + Require Import Arith. - In all forms of rewrite described above, a :token:`term` to rewrite can be - immediately prefixed by one of the following modifiers: + .. coqtop:: out - + `?` : the tactic :n:`rewrite ?@term` performs the rewrite of :token:`term` as many - times as possible (perhaps zero time). This form never fails. - + :n:`@natural?` : works similarly, except that it will do at most :token:`natural` rewrites. - + `!` : works as `?`, except that at least one rewrite should succeed, otherwise - the tactic fails. - + :n:`@natural!` (or simply :n:`@natural`) : precisely :token:`natural` rewrites of :token:`term` will be done, - leading to failure if these :token:`natural` rewrites are not possible. + Lemma example x y : x + y = y + x. - .. tacv:: erewrite @term - :name: erewrite + .. coqtop:: all fail - This tactic works as :n:`rewrite @term` but turning - unresolved bindings into existential variables, if any, instead of - failing. It has the same variants as :tacn:`rewrite` has. + rewrite Nat.add_comm at 2. - .. flag:: Keyed Unification + One can explicitly specify how some variables are bound to match + a different subterm: - Makes higher-order unification used by :tacn:`rewrite` rely on a set of keys to drive - unification. The subterms, considered as rewriting candidates, must start with - the same key as the left- or right-hand side of the lemma given to rewrite, and the arguments - are then unified up to full reduction. + .. coqtop:: all abort -.. tacn:: replace @term with @term’ - :name: replace + rewrite Nat.add_comm with (m := x). - This tactic applies to any goal. It replaces all free occurrences of :n:`@term` - in the current goal with :n:`@term’` and generates an equality :n:`@term = @term’` - as a subgoal. This equality is automatically solved if it occurs among - the assumptions, or if its symmetric form occurs. It is equivalent to - :n:`cut @term = @term’; [intro H`:sub:`n` :n:`; rewrite <- H`:sub:`n` :n:`; clear H`:sub:`n`:n:`|| assumption || symmetry; try assumption]`. + Note that the more advanced :tacn:`setoid_rewrite` tactic + behaves differently, and thus the number of occurrences + available to rewrite may differ between the two tactics. - .. exn:: Terms do not have convertible types. + .. exn:: Tactic failure: Setoid library not loaded. :undocumented: - .. tacv:: replace @term with @term’ by @tactic + .. todo You can use Typeclasses Debug to tell whether rewrite used + setoid rewriting. Example here: https://github.com/coq/coq/pull/13470#discussion_r539230973 - This acts as :n:`replace @term with @term’` but applies :token:`tactic` to solve the generated - subgoal :n:`@term = @term’`. + .. exn:: Cannot find a relation to rewrite. + :undocumented: - .. tacv:: replace @term + .. exn:: Tactic generated a subgoal identical to the original goal. + :undocumented: - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term = @term’` or :n:`@term’ = @term`. + .. exn:: Found no subterm matching @term in @ident. + Found no subterm matching @term in the current goal. - .. tacv:: replace -> @term + This happens if :n:`@term` does not occur in, respectively, the named hypothesis or the goal. - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term = @term’` + .. tacn:: erewrite {+, @oriented_rewriter } {? @occurrences } {? by @ltac_expr3 } - .. tacv:: replace <- @term + Works like :tacn:`rewrite`, but turns + unresolved bindings, if any, into existential variables instead of + failing. It has the same parameters as :tacn:`rewrite`. - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term’ = @term` + .. flag:: Keyed Unification - .. tacv:: replace @term {? with @term} in @goal_occurrences {? by @tactic} - replace -> @term in @goal_occurrences - replace <- @term in @goal_occurrences + Makes higher-order unification used by :tacn:`rewrite` rely on a set of keys to drive + unification. The subterms, considered as rewriting candidates, must start with + the same key as the left- or right-hand side of the lemma given to rewrite, and the arguments + are then unified up to full reduction. - Acts as before but the replacements take place in the specified clauses - (:token:`goal_occurrences`) (see :ref:`performingcomputations`) and not - only in the conclusion of the goal. The clause argument must not contain - any ``type of`` nor ``value of``. +.. tacn:: rewrite * {? {| -> | <- } } @one_term {? in @ident } {? at @rewrite_occs } {? by @ltac_expr3 } + rewrite * {? {| -> | <- } } @one_term at @rewrite_occs in @ident {? by @ltac_expr3 } + :name: rewrite *; _ + :undocumented: - .. tacv:: cutrewrite {? {| <- | -> } } (@term__1 = @term__2) {? in @ident } - :name: cutrewrite +.. tacn:: rewrite_db @ident {? in @ident } + :undocumented: - .. deprecated:: 8.5 +.. tacn:: replace @one_term__from with @one_term__to {? @occurrences } {? by @ltac_expr3 } + replace {? {| -> | <- } } @one_term__from {? @occurrences } + :name: replace; _ - Use :tacn:`replace` instead. + The first form replaces all free occurrences of :n:`@one_term__from` + in the current goal with :n:`@one_term__to` and generates an equality + :n:`@one_term__to = @one_term__from` + as a subgoal. (Note the generated equality is reversed with respect + to the order of the two terms in the tactic syntax; see + issue `#13480 <https://github.com/coq/coq/issues/13480>`_.) + This equality is automatically solved if it occurs among + the hypotheses, or if its symmetric form occurs. -.. tacn:: subst @ident - :name: subst + The second form, with `->` or no arrow, replaces :n:`@one_term__from` + with :n:`@term__to` using + the first hypothesis whose type has the form :n:`@one_term__from = @term__to`. + If `<-` is given, the tactic uses the first hypothesis with the reverse form, + i.e. :n:`@term__to = @one_term__from`. - This tactic applies to a goal that has :n:`@ident` in its context and (at - least) one hypothesis, say :g:`H`, of type :n:`@ident = t` or :n:`t = @ident` - with :n:`@ident` not occurring in :g:`t`. Then it replaces :n:`@ident` by - :g:`t` everywhere in the goal (in the hypotheses and in the conclusion) and - clears :n:`@ident` and :g:`H` from the context. + :n:`@occurrences` + The `type of` and `value of` forms are not supported. + Note you must `Require Setoid` to use the `at` clause in :n:`@occurrences`. - If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also - unfolded and cleared. + :n:`by @ltac_expr3` + Applies the :n:`@ltac_expr3` to solve the generated equality. - If :n:`@ident` is a section variable it is expected to have no - indirect occurrences in the goal, i.e. that no global declarations - implicitly depending on the section variable must be present in the - goal. + .. exn:: Terms do not have convertible types. + :undocumented: - .. note:: - + When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the - first one is used. + .. tacn:: cutrewrite {? {| -> | <- } } @one_term {? in @ident } - + If :g:`H` is itself dependent in the goal, it is replaced by the proof of - reflexivity of equality. + Where :n:`@one_term` is an equality. - .. tacv:: subst {+ @ident} + .. deprecated:: 8.5 - This is equivalent to :n:`subst @ident`:sub:`1`:n:`; ...; subst @ident`:sub:`n`. + Use :tacn:`replace` instead. - .. tacv:: subst +.. tacn:: substitute {? {| -> | <- } } @one_term {? with @bindings } + :undocumented: - This applies :tacn:`subst` repeatedly from top to bottom to all hypotheses of the - context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` - or :n:`@ident := t` exists, with :n:`@ident` not occurring in - ``t`` and :n:`@ident` not a section variable with indirect - dependencies in the goal. +.. tacn:: subst {* @ident } + + For each :n:`@ident`, in order, for which there is a hypothesis in the form + :n:`@ident = @term` or :n:`@term = @ident`, replaces :n:`@ident` with :n:`@term` + everywhere in the hypotheses and the conclusion and clears :n:`@ident` and the hypothesis + from the context. If there are multiple hypotheses that match the :n:`@ident`, + the first one is used. If no :n:`@ident` is given, replacement is done for all + hypotheses in the appropriate form in top to bottom order. + + If :n:`@ident` is a local definition of the form :n:`@ident := @term`, it is also + unfolded and cleared. + + If :n:`@ident` is a section variable it must have no + indirect occurrences in the goal, i.e. no global declarations + implicitly depending on the section variable may be present in the + goal. + + .. note:: + If the hypothesis is itself dependent in the goal, it is replaced by the proof of + reflexivity of equality. .. flag:: Regular Subst Tactic This flag controls the behavior of :tacn:`subst`. When it is activated (it is by default), :tacn:`subst` also deals with the following corner cases: - + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2` - and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not - a variable, and no other hypotheses of the form :n:`@ident`:sub:`2` :n:`= u` - or :n:`u = @ident`:sub:`2`; without the flag, a second call to - subst would be necessary to replace :n:`@ident`:sub:`2` by `t` or + + A context with ordered hypotheses :n:`@ident__1 = @ident__2` + and :n:`@ident__1 = t`, or :n:`t′ = @ident__1` with `t′` not + a variable, and no other hypotheses of the form :n:`@ident__2 = u` + or :n:`u = @ident__2`; without the flag, a second call to + subst would be necessary to replace :n:`@ident__2` by `t` or `t′` respectively. + The presence of a recursive equation which without the flag would be a cause of failure of :tacn:`subst`. - + A context with cyclic dependencies as with hypotheses :n:`@ident`:sub:`1` :n:`= f @ident`:sub:`2` - and :n:`@ident`:sub:`2` :n:`= g @ident`:sub:`1` which without the + + A context with cyclic dependencies as with hypotheses :n:`@ident__1 = f @ident__2` + and :n:`@ident__2 = g @ident__1` which without the flag would be a cause of failure of :tacn:`subst`. - Additionally, it prevents a local definition such as :n:`@ident := t` to be + Additionally, it prevents a local definition such as :n:`@ident := t` from being unfolded which otherwise it would exceptionally unfold in configurations containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident` with `u′` not a variable. Finally, it preserves the initial order of hypotheses, which without the flag it may break. - default. - .. exn:: Cannot find any non-recursive equality over :n:`@ident`. + .. exn:: Cannot find any non-recursive equality over @ident. :undocumented: - .. exn:: Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in hypothesis :n:`@ident`. - Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in the conclusion. + .. exn:: Section variable @ident occurs implicitly in global declaration @qualid present in hypothesis @ident. + Section variable @ident occurs implicitly in global declaration @qualid present in the conclusion. Raised when the variable is a section variable with indirect dependencies in the goal. + If :n:`@ident` is a section variable, it must not have any + indirect occurrences in the goal, i.e. no global declarations + implicitly depending on the section variable may be present in the + goal. +.. tacn:: simple subst + :undocumented: -.. tacn:: stepl @term - :name: stepl +.. tacn:: stepl @one_term {? by @ltac_expr } - This tactic is for chaining rewriting steps. It assumes a goal of the - form :n:`R @term @term` where ``R`` is a binary relation and relies on a + For chaining rewriting steps. It assumes a goal in the + form :n:`R @term__1 @term__2` where ``R`` is a binary relation and relies on a database of lemmas of the form :g:`forall x y z, R x y -> eq x z -> R z y` - where `eq` is typically a setoid equality. The application of :n:`stepl @term` - then replaces the goal by :n:`R @term @term` and adds a new goal stating - :n:`eq @term @term`. + where `eq` is typically a setoid equality. The application of :n:`stepl @one_term` + then replaces the goal by :n:`R @one_term @term__2` and adds a new goal stating + :n:`eq @one_term @term__1`. - .. cmd:: Declare Left Step @term + If :n:`@ltac_expr` is specified, it is applied to the side condition. - Adds :n:`@term` to the database used by :tacn:`stepl`. + .. cmd:: Declare Left Step @one_term + + Adds :n:`@one_term` to the database used by :tacn:`stepl`. This tactic is especially useful for parametric setoids which are not accepted as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see :ref:`Generalizedrewriting`). - .. tacv:: stepl @term by @tactic - - This applies :n:`stepl @term` then applies :token:`tactic` to the second goal. + .. tacn:: stepr @one_term {? by @ltac_expr } - .. tacv:: stepr @term by @tactic - :name: stepr - - This behaves as :tacn:`stepl` but on the right-hand-side of the binary - relation. Lemmas are expected to be of the form + This behaves like :tacn:`stepl` but on the right hand side of the binary + relation. Lemmas are expected to be in the form :g:`forall x y z, R x y -> eq y z -> R x z`. - .. cmd:: Declare Right Step @term + .. cmd:: Declare Right Step @one_term Adds :n:`@term` to the database used by :tacn:`stepr`. +Rewriting with definitional equality +------------------------------------ + +.. tacn:: change {? @one_term__from {? at @occs_nums } with } @one_term__to {? @occurrences } + + Replaces terms with other :term:`convertible` terms. + If :n:`@one_term__from` is not specified, then :n:`@one_term__from` replaces the conclusion and/or + the specified hypotheses. If :n:`@one_term__from` is specified, the tactic replaces occurrences + of :n:`@one_term__to` within the conclusion and/or the specified hypotheses. + + :n:`{? @one_term__from {? at @occs_nums } with }` + Replaces the occurrences of :n:`@one_term__from` specified by :n:`@occs_nums` + with :n:`@one_term__to`, provided that the two :n:`@one_term`\s are + convertible. :n:`@one_term__from` may contain pattern variables such as `?x`, + whose value which will substituted for `x` in :n:`@one_term__to`, such as in + `change (f ?x ?y) with (g (x, y))` or `change (fun x => ?f x) with f`. -.. tacn:: change @term - :name: change + The `at ... with ...` form is deprecated in 8.14; use `with ... at ...` instead. + For `at ... with ... in H |-`, use `with ... in H at ... |-`. - This tactic applies to any goal. It implements the rule ``Conv`` given in - :ref:`subtyping-rules`. :g:`change U` replaces the current goal `T` - with `U` providing that `U` is well-formed and that `T` and `U` are - convertible. + :n:`@occurrences` + If `with` is not specified, :n:`@occurrences` must only specify + entire hypotheses and/or the goal; it must not include any + :n:`at @occs_nums` clauses. .. exn:: Not convertible. :undocumented: - .. tacv:: change @term with @term’ + .. exn:: Found an "at" clause without "with" clause + :undocumented: - This replaces the occurrences of :n:`@term` by :n:`@term’` in the current goal. - The term :n:`@term` and :n:`@term’` must be convertible. + .. tacn:: now_show @one_term - .. tacv:: change @term at {+ @natural} with @term’ + A synonym for :n:`change @one_term`. It can be used to + make some proof steps explicit when refactoring a proof script + to make it readable. - This replaces the occurrences numbered :n:`{+ @natural}` of :n:`@term` by :n:`@term’` - in the current goal. The terms :n:`@term` and :n:`@term’` must be convertible. + .. seealso:: :ref:`Performing computations <performingcomputations>` - .. exn:: Too few occurrences. - :undocumented: +.. tacn:: change_no_check {? @one_term__from {? at @occs_nums } with } @one_term__to {? @occurrences } - .. tacv:: change @term {? {? at {+ @natural}} with @term} in @goal_occurrences + For advanced usage. Similar to :tacn:`change`, but as an optimization, + it skips checking that :n:`@one_term__to` is convertible with the goal or + :n:`@one_term__from`. - 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). + Recall that the Coq kernel typechecks proofs again when they are concluded to + ensure correctness. Hence, using :tacn:`change` checks convertibility twice + overall, while :tacn:`change_no_check` can produce ill-typed terms, + but checks convertibility only once. + Hence, :tacn:`change_no_check` can be useful to speed up certain proof + scripts, especially if one knows by construction that the argument is + indeed convertible to the goal. - .. tacv:: now_show @term + In the following example, :tacn:`change_no_check` replaces :g:`False` with + :g:`True`, but :cmd:`Qed` then rejects the proof, ensuring consistency. - This is a synonym of :n:`change @term`. It can be used to - make some proof steps explicit when refactoring a proof script - to make it readable. + .. example:: - .. seealso:: :ref:`Performing computations <performingcomputations>` + .. coqtop:: all abort fail + + Goal False. + change_no_check True. + exact I. + Qed. + + .. example:: + + .. coqtop:: all abort fail + + Goal True -> False. + intro H. + change_no_check False in H. + exact H. + Qed. .. _performingcomputations: @@ -442,7 +529,10 @@ the conversion in hypotheses :n:`{+ @ident}`. in :cite:`FullReduction`. If Coq is running in native code, it can be typically two to five times faster than :tacn:`vm_compute`. Note however that the compilation cost is higher, so it is worth using only for intensive - computations. + computations. Depending on the configuration, this tactic can either default to + :tacn:`vm_compute`, recompile dependencies or fail due to some missing + precompiled dependencies, + see :ref:`the native-compiler option <native-compiler-options>` for details. .. flag:: NativeCompute Timing @@ -522,7 +612,7 @@ the conversion in hypotheses :n:`{+ @ident}`. use the name of the constant the (co)fixpoint comes from instead of the (co)fixpoint definition in recursive calls. - The :tacn:`cbn` tactic is claimed to be a more principled, faster and more + The :tacn:`cbn` tactic was intended to be a more principled, faster and more predictable replacement for :tacn:`simpl`. The :tacn:`cbn` tactic accepts the same flags as :tacn:`cbv` and @@ -839,10 +929,8 @@ the conversion in hypotheses :n:`{+ @ident}`. Conversion tactics applied to hypotheses ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. tacn:: @tactic in {+, @ident} - - Applies :token:`tactic` (any of the conversion tactics listed in this - section) to the hypotheses :n:`{+ @ident}`. + The form :n:`@tactic in {+, @ident }` applies :token:`tactic` (any of the + conversion tactics listed in this section) to the hypotheses :n:`{+ @ident}`. If :token:`ident` is a local definition, then :token:`ident` can be replaced by :n:`type of @ident` to address not the body but the type of the local diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index df73de846f..609884ce1d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -309,7 +309,7 @@ at the time of use of the notation. a notation should only be used for printing. If a notation to be used both for parsing and printing is - overriden, both the parsing and printing are invalided, even if the + overridden, both the parsing and printing are invalided, even if the overriding rule is only parsing. If a given notation string occurs only in ``only printing`` rules, @@ -588,6 +588,8 @@ As an exception, if the right-hand side is just of the form :n:`@@qualid`, this conventionally stops the inheritance of implicit arguments (but not of notation scopes). +.. _notations-and-binders: + Notations and binders ~~~~~~~~~~~~~~~~~~~~~ @@ -855,7 +857,8 @@ example showing a notation for a chain of equalities. It relies on an artificial expansion of the intended denotation so as to expose a ``φ(x, .. φ(y,t) ..)`` structure, with the drawback that if ever the beta-redexes are contracted, the notations stops to be used for -printing. +printing. Support for notations defined in this way should be considered +experimental. .. coqtop:: in @@ -1070,7 +1073,7 @@ main grammar, or from another custom entry as is the case in Notation "[ e ]" := e (e custom expr at level 2). to indicate that ``e`` has to be parsed at level ``2`` of the grammar -associated to the custom entry ``expr``. The level can be omitted, as in +associated with the custom entry ``expr``. The level can be omitted, as in .. coqdoc:: @@ -1156,7 +1159,6 @@ Similarly, to indicate that a custom entry should parse global references Notation "x" := x (in custom expr at level 0, x global). .. cmd:: Print Custom Grammar @ident - :name: Print Custom Grammar This displays the state of the grammar for terms associated with the custom entry :token:`ident`. @@ -1548,7 +1550,6 @@ Displaying information about scopes Use the :cmd:`Print Visibility` command to display the current notation scope stack. .. cmd:: Print Scope @scope_name - :name: Print Scope Displays all notations defined in the notation scope :n:`@scope_name`. It also displays the delimiting key and the class to which the @@ -1682,7 +1683,6 @@ Number notations ~~~~~~~~~~~~~~~~ .. cmd:: Number Notation @qualid__type @qualid__parse @qualid__print {? ( {+, @number_modifier } ) } : @scope_name - :name: Number Notation .. insertprodn number_modifier number_string_via @@ -1707,6 +1707,8 @@ Number notations * :n:`Number.uint -> option @qualid__type` * :n:`Z -> @qualid__type` * :n:`Z -> option @qualid__type` + * :n:`Int63.int -> @qualid__type` + * :n:`Int63.int -> option @qualid__type` * :n:`Number.number -> @qualid__type` * :n:`Number.number -> option @qualid__type` @@ -1719,6 +1721,8 @@ Number notations * :n:`@qualid__type -> option Number.uint` * :n:`@qualid__type -> Z` * :n:`@qualid__type -> option Z` + * :n:`@qualid__type -> Int63.int` + * :n:`@qualid__type -> option Int63.int` * :n:`@qualid__type -> Number.number` * :n:`@qualid__type -> option Number.number` @@ -1734,7 +1738,8 @@ Number notations Note that only fully-reduced ground terms (terms containing only function application, constructors, inductive type families, - sorts, and primitive integers) will be considered for printing. + sorts, primitive integers, primitive floats, primitive arrays and type + constants for primitive types) will be considered for printing. .. _number-string-via: @@ -1823,16 +1828,23 @@ Number notations only for integers or non-negative integers, and the given number has a fractional or exponent part or is negative. + .. exn:: int63 are only non-negative numbers. + + :n:`Int63.int` are unsigned integers. + + .. exn:: overflow in int63 literal @bigint + + The constant is too big to fit into an unsigned 63-bit integer :n:`Int63.int`. .. exn:: @qualid__parse should go from Number.int to @type or (option @type). Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first). The parsing function given to the :cmd:`Number Notation` - vernacular is not of the right type. + command is not of the right type. .. exn:: @qualid__print should go from @type to Number.int or (option Number.int). Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first). The printing function given to the :cmd:`Number Notation` - vernacular is not of the right type. + command is not of the right type. .. exn:: Unexpected term @term while parsing a number notation. @@ -1862,7 +1874,6 @@ String notations ~~~~~~~~~~~~~~~~ .. cmd:: String Notation @qualid__type @qualid__parse @qualid__print {? ( @number_string_via ) } : @scope_name - :name: String Notation Allows the user to customize how strings are parsed and printed. @@ -1891,7 +1902,8 @@ String notations Note that only fully-reduced ground terms (terms containing only function application, constructors, inductive type families, - sorts, and primitive integers) will be considered for printing. + sorts, primitive integers, primitive floats, primitive arrays and type + constants for primitive types) will be considered for printing. :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]` works as for :ref:`number notations above <number-string-via>`. @@ -1905,12 +1917,12 @@ String notations .. exn:: @qualid__parse should go from Byte.byte or (list Byte.byte) to @type or (option @type). The parsing function given to the :cmd:`String Notation` - vernacular is not of the right type. + command is not of the right type. .. exn:: @qualid__print should go from @type to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)). The printing function given to the :cmd:`String Notation` - vernacular is not of the right type. + command is not of the right type. .. exn:: Unexpected term @term while parsing a string notation. diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst index 93571ecebb..0f0edc6bdd 100644 --- a/doc/sphinx/using/libraries/funind.rst +++ b/doc/sphinx/using/libraries/funind.rst @@ -170,7 +170,6 @@ Tactics ------- .. tacn:: functional induction @term {? using @one_term {? with @bindings } } {? as @simple_intropattern } - :name: functional induction Performs case analysis and induction following the definition of a function :token:`qualid`, which must be fully applied to its arguments as part of @@ -221,7 +220,6 @@ Tactics :undocumented: .. tacn:: functional inversion {| @ident | @natural } {? @qualid } - :name: functional inversion Performs inversion on hypothesis :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst index b68b2ed2a7..78ac17bda1 100644 --- a/doc/sphinx/using/tools/coqdoc.rst +++ b/doc/sphinx/using/tools/coqdoc.rst @@ -34,9 +34,9 @@ Coq material inside documentation. Coq material is quoted between the delimiters ``[`` and ``]``. Square brackets may be nested, the inner ones being understood as being part of the -quoted code (thus you can quote a term like ``fun x => u`` by writing ``[fun -x => u]``). Inside quotations, the code is pretty-printed in the same -way as it is in code parts. +quoted code (thus you can quote a term like ``let id := fun [T : Type] (x : t) => x in id 0`` +by writing ``[let id := fun [T : Type] (x : t) => x in id 0]``). +Inside quotations, the code is pretty-printed the same way as in code parts. Preformatted vernacular is enclosed by ``[[`` and ``]]``. The former must be followed by a newline and the latter must follow a newline. diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 56464851ba..fa739e97bc 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -99,6 +99,11 @@ def make_math_node(latex, docname, nowrap): node['number'] = None return node +# To support any character in tacn, ... names. +# see https://github.com/coq/coq/pull/13564 +def make_id(tag): + return tag.replace(" ", "-") + class CoqObject(ObjectDescription): """A generic Coq object for Sphinx; all Coq objects are subclasses of this. @@ -200,7 +205,7 @@ class CoqObject(ObjectDescription): names_in_subdomain[name] = (self.env.docname, self.objtype, target_id) def _target_id(self, name): - return make_target(self.objtype, nodes.make_id(name)) + return make_target(self.objtype, make_id(name)) def _add_target(self, signode, name): """Register a link target ‘name’, pointing to signode.""" @@ -210,6 +215,13 @@ class CoqObject(ObjectDescription): signode['names'].append(name) signode['first'] = (not self.names) self._record_name(name, targetid, signode) + else: + # todo: make the following a real error or warning + # todo: then maybe the above "if" is not needed + names_in_subdomain = self.subdomain_data() + if name in names_in_subdomain: + print("Duplicate", self.subdomain, "name: ", name) + # self._warn_if_duplicate_name(names_in_subdomain, name, signode) return targetid def _add_index_entry(self, name, target): @@ -322,7 +334,7 @@ class VernacObject(NotationObject): annotation = "Command" def _name_from_signature(self, signature): - m = re.match(r"[a-zA-Z ]+", signature) + m = re.match(r"[a-zA-Z0-9_ ]+", signature) return m.group(0).strip() if m else None class VernacVariantObject(VernacObject): @@ -333,7 +345,7 @@ class VernacVariantObject(VernacObject): .. cmd:: Axiom @ident : @term. This command links :token:`term` to the name :token:`term` as its specification in - the global context. The fact asserted by :token:`term` is thus assumed as a + the global environment. The fact asserted by :token:`term` is thus assumed as a postulate. .. cmdv:: Parameter @ident : @term. @@ -505,7 +517,7 @@ class ProductionObject(CoqObject): pass def _target_id(self, name): - return 'grammar-token-{}'.format(nodes.make_id(name[1])) + return make_id('grammar-token-{}'.format(name[1])) def _record_name(self, name, targetid, signode): env = self.state.document.settings.env @@ -533,7 +545,7 @@ class ProductionObject(CoqObject): row = nodes.container(classes=['prodn-row']) entry = nodes.container(classes=['prodn-cell-nonterminal']) if lhs != "": - target_name = 'grammar-token-' + nodes.make_id(lhs) + target_name = make_id('grammar-token-' + lhs) target = nodes.target('', '', ids=[target_name], names=[target_name]) # putting prodn-target on the target node won't appear in the tex file inline = nodes.inline(classes=['prodn-target']) @@ -862,7 +874,7 @@ class InferenceDirective(Directive): docname = self.state.document.settings.env.docname math_node = make_math_node(latex, docname, nowrap=False) - tid = nodes.make_id(title) + tid = make_id(title) target = nodes.target('', '', ids=['inference-' + tid]) self.state.document.note_explicit_target(target) @@ -1182,7 +1194,7 @@ def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, conte """ #pylint: disable=dangerous-default-value, unused-argument env = inliner.document.settings.env - targetid = nodes.make_id('grammar-token-{}'.format(text)) + targetid = make_id('grammar-token-{}'.format(text)) target = nodes.target('', '', ids=[targetid]) inliner.document.note_explicit_target(target) code = nodes.literal(rawtext, text, role=typ.lower()) @@ -1221,7 +1233,7 @@ def GlossaryDefRole(typ, rawtext, text, lineno, inliner, options={}, content=[]) msg = MSG.format(term, env.doc2path(std[key][0])) inliner.document.reporter.warning(msg, line=lineno) - targetid = nodes.make_id('term-{}'.format(term)) + targetid = make_id('term-{}'.format(term)) std[key] = (env.docname, targetid) target = nodes.target('', '', ids=[targetid], names=[term]) inliner.document.note_explicit_target(target) diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py index 3021594183..388efd01d6 100644 --- a/doc/tools/coqrst/repl/coqtop.py +++ b/doc/tools/coqrst/repl/coqtop.py @@ -52,7 +52,7 @@ class CoqTop: self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN', ""), "coqtop") if not pexpect.utils.which(self.coqtop_bin): raise ValueError("coqtop binary not found: '{}'".format(self.coqtop_bin)) - self.args = (args or []) + ["-color", "on"] * color + self.args = (args or []) + ["-q"] + ["-color", "on"] * color self.coqtop = None def __enter__(self): diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 75b3260166..27144fd1ad 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -447,7 +447,7 @@ binder: [ open_binders: [ | REPLACE name LIST0 name ":" lconstr -| WITH LIST1 name ":" lconstr +| WITH LIST1 name ":" type (* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *) | DELETE name ".." name | REPLACE name LIST0 name binders @@ -864,8 +864,8 @@ ltac_expr1: [ | EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end" | MOVETO simple_tactic match_key OPT "reverse" "goal" "with" match_context_list "end" | MOVETO simple_tactic match_key ltac_expr5 "with" match_list "end" -| REPLACE failkw [ int_or_var | ] LIST0 message_token -| WITH failkw OPT int_or_var LIST0 message_token +| REPLACE failkw [ nat_or_var | ] LIST0 message_token +| WITH failkw OPT nat_or_var LIST0 message_token | REPLACE reference LIST0 tactic_arg | WITH reference LIST1 tactic_arg | l1_tactic @@ -1003,7 +1003,7 @@ simple_tactic: [ | DELETE "replace" uconstr clause | "replace" orient uconstr clause | REPLACE "rewrite" "*" orient uconstr "in" hyp "at" occurrences by_arg_tac -| WITH "rewrite" "*" orient uconstr OPT ( "in" hyp ) OPT ( "at" occurrences by_arg_tac ) +| WITH "rewrite" "*" orient uconstr OPT ( "in" hyp ) OPT ( "at" occurrences ) by_arg_tac | DELETE "rewrite" "*" orient uconstr "in" hyp by_arg_tac | DELETE "rewrite" "*" orient uconstr "at" occurrences by_arg_tac | DELETE "rewrite" "*" orient uconstr by_arg_tac @@ -1510,8 +1510,6 @@ query_command: [ | WITH "Check" lconstr | REPLACE "About" smart_global OPT univ_name_list "." | WITH "About" smart_global OPT univ_name_list -| REPLACE "SearchHead" constr_pattern in_or_out_modules "." -| WITH "SearchHead" constr_pattern in_or_out_modules | REPLACE "SearchPattern" constr_pattern in_or_out_modules "." | WITH "SearchPattern" constr_pattern in_or_out_modules | REPLACE "SearchRewrite" constr_pattern in_or_out_modules "." @@ -1814,6 +1812,7 @@ ltac_defined_tactics: [ | "lia" | "lra" | "nia" +| "now_show" constr | "nra" | "over" TAG SSR | "split_Rabs" @@ -2065,7 +2064,7 @@ ltac2_tactic_atom: [ | MOVETO ltac2_quotations "constr" ":" "(" lconstr ")" (* Ltac2 plugin *) | MOVETO ltac2_quotations "open_constr" ":" "(" lconstr ")" (* Ltac2 plugin *) | MOVETO ltac2_quotations "ident" ":" "(" lident ")" (* Ltac2 plugin *) -| MOVETO ltac2_quotations "pattern" ":" "(" cpattern ")" (* Ltac2 plugin *) +| MOVETO ltac2_quotations "pat" ":" "(" cpattern ")" (* Ltac2 plugin *) | MOVETO ltac2_quotations "reference" ":" "(" globref ")" (* Ltac2 plugin *) | MOVETO ltac2_quotations "ltac1" ":" "(" ltac1_expr_in_env ")" (* Ltac2 plugin *) | MOVETO ltac2_quotations "ltac1val" ":" "(" ltac1_expr_in_env ")" (* Ltac2 plugin *) @@ -2373,7 +2372,7 @@ ssrapplyarg: [ ] constr_with_bindings_arg: [ -| EDIT ADD_OPT ">" constr_with_bindings TAG SSR +| EDIT ADD_OPT ">" constr_with_bindings ] destruction_arg: [ @@ -2469,6 +2468,15 @@ variance_identref: [ | EDIT ADD_OPT variance identref ] +conversion: [ +| DELETE constr +| DELETE constr "with" constr +| PRINT +| REPLACE constr "at" occs_nums "with" constr +| WITH OPT ( constr OPT ( "at" occs_nums ) "with" ) constr +| PRINT +] + SPLICE: [ | clause | noedit_mode @@ -2694,6 +2702,8 @@ SPLICE: [ | cumul_ident_decl | variance | variance_identref +| rewriter +| conversion ] (* end SPLICE *) RENAME: [ @@ -2751,6 +2761,7 @@ RENAME: [ | pattern_occ pattern_occs | hypident_occ hyp_occs | concl_occ concl_occs +| constr_with_bindings_arg one_term_with_bindings ] simple_tactic: [ diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index dd7990368e..a1c1d87763 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -1726,8 +1726,6 @@ let process_rst g file args seen tac_prods cmd_prods = let cmd_exclude_files = [ "doc/sphinx/proof-engine/ssreflect-proof-language.rst"; - "doc/sphinx/proofs/writing-proofs/rewriting.rst"; - "doc/sphinx/proofs/writing-proofs/proof-mode.rst"; "doc/sphinx/proof-engine/tactics.rst"; ] in diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index ccf38d2c15..bc6b803bbb 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -687,17 +687,6 @@ command: [ | "Add" "Zify" "BinOpSpec" constr (* micromega plugin *) | "Add" "Zify" "UnOpSpec" constr (* micromega plugin *) | "Add" "Zify" "Saturate" constr (* micromega plugin *) -| "Add" "InjTyp" constr (* micromega plugin *) -| "Add" "BinOp" constr (* micromega plugin *) -| "Add" "UnOp" constr (* micromega plugin *) -| "Add" "CstOp" constr (* micromega plugin *) -| "Add" "BinRel" constr (* micromega plugin *) -| "Add" "PropOp" constr (* micromega plugin *) -| "Add" "PropBinOp" constr (* micromega plugin *) -| "Add" "PropUOp" constr (* micromega plugin *) -| "Add" "BinOpSpec" constr (* micromega plugin *) -| "Add" "UnOpSpec" constr (* micromega plugin *) -| "Add" "Saturate" constr (* micromega plugin *) | "Show" "Zify" "InjTyp" (* micromega plugin *) | "Show" "Zify" "BinOp" (* micromega plugin *) | "Show" "Zify" "UnOp" (* micromega plugin *) @@ -705,7 +694,6 @@ command: [ | "Show" "Zify" "BinRel" (* micromega plugin *) | "Show" "Zify" "UnOpSpec" (* micromega plugin *) | "Show" "Zify" "BinOpSpec" (* micromega plugin *) -| "Show" "Zify" "Spec" (* micromega plugin *) | "Add" "Ring" ident ":" constr OPT ring_mods (* ring plugin *) | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" constr OPT field_mods (* ring plugin *) @@ -1258,7 +1246,6 @@ query_command: [ | "Compute" lconstr "." | "Check" lconstr "." | "About" smart_global OPT univ_name_list "." -| "SearchHead" constr_pattern in_or_out_modules "." | "SearchPattern" constr_pattern in_or_out_modules "." | "SearchRewrite" constr_pattern in_or_out_modules "." | "Search" search_query search_queries "." @@ -1551,7 +1538,6 @@ simple_tactic: [ | "revert" LIST1 hyp | "simple" "induction" quantified_hypothesis | "simple" "destruct" quantified_hypothesis -| "double" "induction" quantified_hypothesis quantified_hypothesis | "admit" | "fix" ident natural | "cofix" ident @@ -1669,7 +1655,6 @@ simple_tactic: [ | "autounfold_one" hintbases | "unify" constr constr | "unify" constr constr "with" preident -| "convert_concl_no_check" constr | "typeclasses" "eauto" "bfs" OPT nat_or_var "with" LIST1 preident | "typeclasses" "eauto" OPT nat_or_var "with" LIST1 preident | "typeclasses" "eauto" "bfs" OPT nat_or_var @@ -2095,7 +2080,7 @@ ltac_expr1: [ | "first" "[" LIST0 ltac_expr5 SEP "|" "]" | "solve" "[" LIST0 ltac_expr5 SEP "|" "]" | "idtac" LIST0 message_token -| failkw [ int_or_var | ] LIST0 message_token +| failkw [ nat_or_var | ] LIST0 message_token | simple_tactic | tactic_value | reference LIST0 tactic_arg @@ -3370,7 +3355,7 @@ G_LTAC2_tactic_atom: [ | "constr" ":" "(" Constr.lconstr ")" (* Ltac2 plugin *) | "open_constr" ":" "(" Constr.lconstr ")" (* Ltac2 plugin *) | "ident" ":" "(" lident ")" (* Ltac2 plugin *) -| "pattern" ":" "(" Constr.cpattern ")" (* Ltac2 plugin *) +| "pat" ":" "(" Constr.cpattern ")" (* Ltac2 plugin *) | "reference" ":" "(" globref ")" (* Ltac2 plugin *) | "ltac1" ":" "(" ltac1_expr_in_env ")" (* Ltac2 plugin *) | "ltac1val" ":" "(" ltac1_expr_in_env ")" (* Ltac2 plugin *) diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index d950b32160..a34e96ac16 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -493,7 +493,7 @@ term_forall_or_fun: [ ] open_binders: [ -| LIST1 name ":" term +| LIST1 name ":" type | LIST1 binder ] @@ -1001,18 +1001,6 @@ command: [ | "Reset" "Ltac" "Profile" | "Show" "Ltac" "Profile" OPT [ "CutOff" integer | string ] | "Show" "Lia" "Profile" (* micromega plugin *) -| "Add" "InjTyp" one_term (* micromega plugin *) -| "Add" "BinOp" one_term (* micromega plugin *) -| "Add" "UnOp" one_term (* micromega plugin *) -| "Add" "CstOp" one_term (* micromega plugin *) -| "Add" "BinRel" one_term (* micromega plugin *) -| "Add" "PropOp" one_term (* micromega plugin *) -| "Add" "PropBinOp" one_term (* micromega plugin *) -| "Add" "PropUOp" one_term (* micromega plugin *) -| "Add" "BinOpSpec" one_term (* micromega plugin *) -| "Add" "UnOpSpec" one_term (* micromega plugin *) -| "Add" "Saturate" one_term (* micromega plugin *) -| "Show" "Zify" "Spec" (* micromega plugin *) | "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" ) (* ring plugin *) | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* ring plugin *) @@ -1117,7 +1105,6 @@ command: [ | "Compute" term | "Check" term | "About" reference OPT univ_name_list -| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid ) @@ -1247,11 +1234,7 @@ lident: [ destruction_arg: [ | natural -| constr_with_bindings_arg -] - -constr_with_bindings_arg: [ -| OPT ">" one_term OPT ( "with" bindings ) (* SSR plugin *) +| one_term_with_bindings ] occurrences: [ @@ -1630,7 +1613,6 @@ simple_tactic: [ | "revert" LIST1 ident | "simple" "induction" [ ident | natural ] | "simple" "destruct" [ ident | natural ] -| "double" "induction" [ ident | natural ] [ ident | natural ] | "admit" | "clear" LIST0 ident | "clear" "-" LIST1 ident @@ -1657,7 +1639,7 @@ simple_tactic: [ | "first" "[" LIST0 ltac_expr SEP "|" "]" | "solve" "[" LIST0 ltac_expr SEP "|" "]" | "idtac" LIST0 [ ident | string | natural ] -| [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | natural ] +| [ "fail" | "gfail" ] OPT nat_or_var LIST0 [ ident | string | natural ] | ltac_expr ssrintros (* SSR plugin *) | "fun" LIST1 name "=>" ltac_expr | "eval" red_expr "in" term @@ -1691,7 +1673,7 @@ simple_tactic: [ | "absurd" one_term | "contradiction" OPT ( one_term OPT ( "with" bindings ) ) | "autorewrite" OPT "*" "with" LIST1 ident OPT occurrences OPT ( "using" ltac_expr ) -| "rewrite" "*" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) OPT ( "at" rewrite_occs OPT ( "by" ltac_expr3 ) ) +| "rewrite" "*" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) OPT ( "at" rewrite_occs ) OPT ( "by" ltac_expr3 ) | "rewrite" "*" OPT [ "->" | "<-" ] one_term "at" rewrite_occs "in" ident OPT ( "by" ltac_expr3 ) | "refine" one_term | "simple" "refine" one_term @@ -1762,7 +1744,6 @@ simple_tactic: [ | "autounfold" OPT hintbases OPT occurrences | "autounfold_one" OPT hintbases OPT ( "in" ident ) | "unify" one_term one_term OPT ( "with" ident ) -| "convert_concl_no_check" one_term | "typeclasses" "eauto" OPT "bfs" OPT nat_or_var OPT ( "with" LIST1 ident ) | "head_of_constr" ident one_term | "not_evar" one_term @@ -1783,12 +1764,12 @@ simple_tactic: [ | "eintros" LIST0 intropattern | "decide" "equality" | "compare" one_term one_term -| "apply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as -| "eapply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as -| "simple" "apply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as -| "simple" "eapply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as -| "elim" constr_with_bindings_arg OPT ( "using" one_term OPT ( "with" bindings ) ) -| "eelim" constr_with_bindings_arg OPT ( "using" one_term OPT ( "with" bindings ) ) +| "apply" LIST1 one_term_with_bindings SEP "," OPT in_hyp_as +| "eapply" LIST1 one_term_with_bindings SEP "," OPT in_hyp_as +| "simple" "apply" LIST1 one_term_with_bindings SEP "," OPT in_hyp_as +| "simple" "eapply" LIST1 one_term_with_bindings SEP "," OPT in_hyp_as +| "elim" one_term_with_bindings OPT ( "using" one_term OPT ( "with" bindings ) ) +| "eelim" one_term_with_bindings OPT ( "using" one_term OPT ( "with" bindings ) ) | "case" induction_clause_list | "ecase" induction_clause_list | "fix" ident natural OPT ( "with" LIST1 fixdecl ) @@ -1842,8 +1823,8 @@ simple_tactic: [ | "unfold" LIST1 reference_occs SEP "," OPT occurrences | "fold" LIST1 one_term OPT occurrences | "pattern" LIST1 pattern_occs SEP "," OPT occurrences -| "change" conversion OPT occurrences -| "change_no_check" conversion OPT occurrences +| "change" OPT ( one_term OPT ( "at" occs_nums ) "with" ) one_term OPT occurrences +| "change_no_check" OPT ( one_term OPT ( "at" occs_nums ) "with" ) one_term OPT occurrences | "btauto" | "rtauto" | "congruence" OPT natural OPT ( "with" LIST1 one_term ) @@ -1922,6 +1903,7 @@ simple_tactic: [ | "lia" | "lra" | "nia" +| "now_show" one_term | "nra" | "over" (* SSR plugin *) | "split_Rabs" @@ -1977,11 +1959,11 @@ as_name: [ ] oriented_rewriter: [ -| OPT [ "->" | "<-" ] rewriter +| OPT [ "->" | "<-" ] OPT natural OPT [ "?" | "!" ] one_term_with_bindings ] -rewriter: [ -| OPT natural OPT [ "?" | "!" ] constr_with_bindings_arg +one_term_with_bindings: [ +| OPT ">" one_term OPT ( "with" bindings ) ] induction_clause_list: [ @@ -2381,7 +2363,7 @@ ltac2_quotations: [ | "ident" ":" "(" lident ")" | "constr" ":" "(" term ")" | "open_constr" ":" "(" term ")" -| "pattern" ":" "(" cpattern ")" +| "pat" ":" "(" cpattern ")" | "reference" ":" "(" [ "&" ident | qualid ] ")" | "ltac1" ":" "(" ltac1_expr_in_env ")" | "ltac1val" ":" "(" ltac1_expr_in_env ")" @@ -2423,7 +2405,6 @@ tac2mode: [ | "Compute" term | "Check" term | "About" reference OPT univ_name_list -| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid ) @@ -2454,12 +2435,6 @@ cofixdecl: [ | "(" ident LIST0 simple_binder ":" term ")" ] -conversion: [ -| one_term -| one_term "with" one_term -| one_term "at" occs_nums "with" one_term -] - func_scheme_def: [ | ident ":=" "Induction" "for" qualid "Sort" sort_family (* funind plugin *) ] |