diff options
Diffstat (limited to 'doc/sphinx/proof-engine/ltac.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index dc9add66f9..d81048f075 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1092,7 +1092,7 @@ Basically, |Ltac| toplevel definitions are made as follows: Printing |Ltac| tactics ~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Print Ltac @qualid. +.. cmd:: Print Ltac @qualid Defined |Ltac| functions can be displayed using this command. |