diff options
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index ae3a252570..d9a0178cce 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1730,6 +1730,8 @@ Defining |Ltac| symbols |Ltac| toplevel definitions are made as follows: +.. index:: ::= + .. cmd:: Ltac @tacdef_body {* with @tacdef_body } :name: Ltac |