diff options
Diffstat (limited to 'doc/sphinx/proof-engine/tactics.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 90ca0da432..29c2f8b815 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -971,7 +971,7 @@ quantification or an implication. move H0 before H. .. tacn:: rename @ident into @ident - :name: rename ... into ... + :name: rename This renames hypothesis :n:`@ident` into :n:`@ident` in the current context. The name of the hypothesis in the proof-term, however, is left unchanged. |