diff options
| author | Clément Pit-Claudel | 2019-02-14 13:49:43 -0500 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-02-14 13:49:43 -0500 |
| commit | 5ea4369bd4604b61ccc669f136827299920fb635 (patch) | |
| tree | 20bf0291452f70d003627112fe88b94dff22714a /doc | |
| parent | 7831c257168b74fc8e7132af2ec0b7a8aa00d539 (diff) | |
| parent | 57c69e8b78df99e69a31c0a6129346915de5e38c (diff) | |
Merge PR #9571: Document the now_show tactic.
Ack-by: Zimmi48
Reviewed-by: cpitclaudel
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index d58cbdec07..6f57cc53a9 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2957,6 +2957,12 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. + .. tacv:: now_show @term + + This is a synonym of :n:`change @term`. It can be used to + make some proof steps explicit when refactoring a proof script + to make it readable. + .. seealso:: :ref:`Performing computations <performingcomputations>` .. _performingcomputations: |