diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-24 11:59:48 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-05 11:54:02 +0200 |
| commit | 98b79e9bf4ac082f948e381a68b8219fc3f3c314 (patch) | |
| tree | 14115f55fae32c99a0546e07eefa9b589667bcbf | |
| parent | 7a569dfe04e62a97780c7f5f9e4f225b82c8f96a (diff) | |
[sphinx] Backport reformulation.
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 6c1b1c08c..76796c934 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2430,8 +2430,8 @@ subgoals. 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`:sub:`i` for all hypotheses - :g:`H`:sub:`i` :g:`<> H`. A success will happen as soon as at least one of these - simpler tactics succeeds. + :g:`H`:sub:`i` 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. |