From e16bbf716b97128272556134b88da2e80c3d115d Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Fri, 8 Jan 2021 12:06:24 -0800 Subject: Improve doc of occurrences and rewrite. --- doc/sphinx/proofs/writing-proofs/rewriting.rst | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'doc/sphinx/proofs') diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 07b7928847..874c3a8f4d 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 `, even for Leibniz’s equality. + :ref:`setoid rewriting `, 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. -- cgit v1.2.3