diff options
| author | Théo Winterhalter | 2018-06-01 08:19:09 +0200 |
|---|---|---|
| committer | Théo Winterhalter | 2018-06-01 08:19:09 +0200 |
| commit | 5407d7ed952b174cba9ad7e3362d1e1b364d2178 (patch) | |
| tree | e7274a83a57917bba97968f0809b7e8ad6df800f | |
| parent | 1967ddb1fb4eb250b2bb10c9f8fbdc56fa954fe1 (diff) | |
Merge two clearbody docs
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 11 |
1 files 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 |