aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/proof-engine
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-04 10:26:38 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-04 10:26:38 +0200
commit2837bab8a84395f07f53513319b82168a68305ca (patch)
tree3aabc6b5485e876b7b2efa9d729d0c6e4d962736 /doc/sphinx/proof-engine
parentf0afda002a4faaecdddff09593ee404ea5a602b0 (diff)
parent5407d7ed952b174cba9ad7e3362d1e1b364d2178 (diff)
Merge PR #7648: Indicate in the doc that clearbody can take several idents
Diffstat (limited to 'doc/sphinx/proof-engine')
-rw-r--r--doc/sphinx/proof-engine/tactics.rst17
1 files changed, 9 insertions, 8 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index da4c3f9d7..051c28f91 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -879,14 +879,6 @@ quantification or an implication.
This is equivalent to :n:`clear @ident. ... clear @ident.`
-.. tacv:: clearbody @ident
- :name: clearbody
-
- This tactic expects :n:`@ident` to be a local definition then clears its
- body. Otherwise said, this tactic turns a definition into an assumption.
-
-.. exn:: @ident is not a local definition.
-
.. tacv:: clear - {+ @ident}
This tactic clears all the hypotheses except the ones depending in the
@@ -901,6 +893,15 @@ quantification or an implication.
This clears the hypothesis :n:`@ident` and all the hypotheses that depend on
it.
+.. tacv:: clearbody {+ @ident}
+ :name: clearbody
+
+ This tactic expects :n:`{+ @ident}` to be local definitions and clears their
+ respective bodies.
+ In other words, it turns the given definitions into assumptions.
+
+.. exn:: @ident is not a local definition.
+
.. tacn:: revert {+ @ident}
:name: revert