diff options
Diffstat (limited to 'doc')
27 files changed, 302 insertions, 282 deletions
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/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/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/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/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/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/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index c54db36691..9ac05fab2e 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -726,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 ~~~~~~~~~~~ @@ -773,7 +797,7 @@ are applied using the tactic :n:`rewrite_strat @rewstrategy`. failure :n:`id` - identity + identity :n:`refl` reflexivity @@ -803,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 @@ -833,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)` @@ -876,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/micromega.rst b/doc/sphinx/addendum/micromega.rst index 38c4886e0f..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 @@ -315,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/program.rst b/doc/sphinx/addendum/program.rst index 2b24ced8a1..8f2b51ccce 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -320,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/changes.rst b/doc/sphinx/changes.rst index d9e4e4f2b3..ea099eb52e 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -531,11 +531,11 @@ Commands and options .. _813HintWarning: - **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 + 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:** @@ -701,6 +701,27 @@ Commands and options (`#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 ------------ @@ -1230,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 @@ -1301,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:** @@ -3191,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 diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index 8dbc1626ba..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 diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 0a61c4ce22..2b50d4c420 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -523,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/modules.rst b/doc/sphinx/language/core/modules.rst index 93d70c773f..2e678c49d8 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -880,7 +880,7 @@ started, unless option ``-top`` or ``-notop`` is set (see :ref:`command-line-opt .. _qualified-names: Qualified identifiers ---------------------- +~~~~~~~~~~~~~~~~~~~~~ .. insertprodn qualid field_ident @@ -1010,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/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/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 3646a32a79..1bb4216e4f 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -554,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 ) @@ -568,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, diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 766f7ab44e..665bae7077 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -77,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 @@ -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. @@ -2067,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 diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 8e2f577f6b..8db16fff69 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -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 @@ -384,7 +359,7 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). .. table:: Search Blacklist @string 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_``. @@ -395,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. @@ -1083,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 d7228a3907..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: diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 8873d02888..f286533d78 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -44,11 +44,14 @@ Rewriting with Leibniz and setoid equality oriented_rewriter ::= {? {| -> | <- } } {? @natural } {? {| ? | ! } } @one_term_with_bindings one_term_with_bindings ::= {? > } @one_term {? with @bindings } - Rewrites terms based on equalities. The type of :n:`@one_term` must have the form: + Replaces subterms with other subterms that have been proven to be equal. + The type of :n:`@one_term` must have the form: :n:`{? forall {+ (x__i: A__i) } , } EQ @term__1 @term__2` - where :g:`EQ` is the Leibniz equality `eq` or a registered setoid equality. + .. todo :term:`Leibniz equality` does not work with Sphinx 2.3.1. It does with Sphinx 3.0.3. + + 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>`. @@ -61,7 +64,7 @@ Rewriting with Leibniz and setoid equality 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 :tacn:`setoid_rewrite` + to variables bound by the `forall`; use the more advanced :tacn:`setoid_rewrite` if you want to find such occurrences. :n:`{+, @oriented_rewriter }` @@ -90,12 +93,55 @@ Rewriting with Leibniz and setoid equality any of them can be rewritten. If not specified, only the first occurrence in the conclusion is replaced. - If :n:`at @occs_nums` is specified, rewriting is always done with - :ref:`setoid rewriting <generalizedrewriting>`, even for Leibniz’s equality. + .. note:: + + 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). :n:`by @ltac_expr3` If specified, is used to resolve all side conditions generated by the tactic. + .. note:: + + 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`). + + For instance, if we want to rewrite the right-hand side in the + following goal, this will not work: + + .. coqtop:: none + + Require Import Arith. + + .. coqtop:: out + + Lemma example x y : x + y = y + x. + + .. coqtop:: all fail + + rewrite Nat.add_comm at 2. + + One can explicitly specify how some variables are bound to match + a different subterm: + + .. coqtop:: all abort + + rewrite Nat.add_comm with (m := x). + + 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:: Tactic failure: Setoid library not loaded. :undocumented: @@ -338,13 +384,6 @@ Rewriting with definitional equality exact H. Qed. - .. tacn:: convert_concl_no_check @one_term - - .. deprecated:: 8.11 - - Deprecated old name for :tacn:`change_no_check`. Does not support any of its - variants. - .. _performingcomputations: Performing computations @@ -890,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/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 44bb767011..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 @@ -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 "." @@ -2066,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 *) diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 9f2559ffbc..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 @@ -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 b53af609ec..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 ) @@ -1626,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 @@ -1758,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 @@ -2378,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 ")" @@ -2420,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 ) |