From 1967ddb1fb4eb250b2bb10c9f8fbdc56fa954fe1 Mon Sep 17 00:00:00 2001
From: Théo Winterhalter
Date: Thu, 31 May 2018 10:58:39 +0200
Subject: Indicate in the doc that clearbody can take several idents

---
 doc/sphinx/proof-engine/tactics.rst | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index da4c3f9d74..110e3253e7 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
 
-- 
cgit v1.2.3


From 5407d7ed952b174cba9ad7e3362d1e1b364d2178 Mon Sep 17 00:00:00 2001
From: Théo Winterhalter
Date: Fri, 1 Jun 2018 08:19:09 +0200
Subject: Merge two clearbody docs

---
 doc/sphinx/proof-engine/tactics.rst | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 110e3253e7..051c28f910 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -893,18 +893,15 @@ quantification or an implication.
    This clears the hypothesis :n:`@ident` and all the hypotheses that depend on
    it.
 
-.. tacv:: clearbody @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.
+   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.
 
-.. tacv:: clearbody {+ @ident}
-
-   This is equivalent to :n:`clearbody @ident. ... clearbody @ident.`
-
 .. tacn:: revert {+ @ident}
    :name: revert
 
-- 
cgit v1.2.3