From 57c69e8b78df99e69a31c0a6129346915de5e38c Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 13 Feb 2019 18:33:46 +0100 Subject: Document the now_show tactic. It was used in the standard library and the test-suite but undocumented so far. --- doc/sphinx/proof-engine/tactics.rst | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'doc/sphinx/proof-engine') 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: -- cgit v1.2.3