diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index c1eb1f974c..8418e9c73d 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -174,6 +174,14 @@ mode but it can also be used in toplevel definitions as shown below. ltac_def : `ident` [`ident` ... `ident`] := `ltac_expr` : `qualid` [`ident` ... `ident`] ::= `ltac_expr` +Tactics in terms +~~~~~~~~~~~~~~~~ + +.. insertprodn term_ltac term_ltac + +.. prodn:: + term_ltac ::= ltac : ( @ltac_expr ) + .. _ltac-semantics: Semantics |