diff options
| author | coqbot-app[bot] | 2021-01-22 21:18:09 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-22 21:18:09 +0000 |
| commit | 03ce01464a36426f152040c85c9b8cf11b0766fc (patch) | |
| tree | 9f6f4f84c791c19110996b8cdc0681e9c92d3b5d /doc | |
| parent | 5986422fe75d017f75a0223f348d264638c1e33c (diff) | |
| parent | e16bbf716b97128272556134b88da2e80c3d115d (diff) | |
Merge PR #13754: Improve doc of occurrences and rewrite.
Reviewed-by: Zimmi48
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 5 |
2 files changed, 14 insertions, 5 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 766f7ab44e..25efca563a 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. diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 0a4a48555f..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. |