diff options
| author | Théo Zimmermann | 2019-02-13 18:33:46 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-14 10:25:01 +0100 |
| commit | 57c69e8b78df99e69a31c0a6129346915de5e38c (patch) | |
| tree | d200356b778cbf43f1dccb23e38a9418aba6164a | |
| parent | aa2d7486702433c94bfd645d3a5f6575a9ee729f (diff) | |
Document the now_show tactic.
It was used in the standard library and the test-suite but undocumented so far.
| -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 0bcfce2322..e280ab0f34 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2933,6 +2933,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: |