diff options
| author | Théo Zimmermann | 2020-11-09 16:34:39 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-11-09 16:42:02 +0100 |
| commit | 3f5f5cf07de6eb804e52da8213a0f1a75cb0cdbe (patch) | |
| tree | f3a976146d19c349b310d7f468ddedbb1a357fc3 /doc/sphinx/proof-engine | |
| parent | c0b48997dc7fccd15ab237df6274dbcfa05cbc9c (diff) | |
Fix #5226: Add index entry for ::=.
Diffstat (limited to 'doc/sphinx/proof-engine')
| -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 |