Indicate in the doc that clearbody can take several idents

1 files changed, 12 insertions, 8 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index da4c3f9d7..110e3253e 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,18 @@ 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 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:: clearbody {+ @ident}
+
+   This is equivalent to :n:`clearbody @ident. ... clearbody @ident.`
+
 .. tacn:: revert {+ @ident}
    :name: revert