diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 62 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/detailed-tactic-examples.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 27 | ||||
| -rw-r--r-- | doc/sphinx/proofs/automatic-tactics/auto.rst | 13 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 18 |
6 files changed, 32 insertions, 104 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 38c4886e0f..3bd85d29c8 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -315,68 +315,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/changes.rst b/doc/sphinx/changes.rst index fc40ba0249..58444e8e82 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:** @@ -3191,7 +3191,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/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/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 766f7ab44e..72970f46b0 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -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/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..663337bc64 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -91,7 +91,10 @@ Rewriting with Leibniz and setoid equality 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. + :ref:`setoid rewriting <generalizedrewriting>`, even for Leibniz’s 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 already mentioned above). :n:`by @ltac_expr3` If specified, is used to resolve all side conditions generated by the tactic. @@ -338,13 +341,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 +886,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 |