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(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 110e3253e..051c28f91 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