diff options
| author | Hugo Herbelin | 2019-11-13 20:54:52 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-06 17:04:11 +0200 |
| commit | 986bfd1ff69231f1b17efda2fa5d13b88a39caee (patch) | |
| tree | 0868872b9517fe66cb9388dd2c871f8a61e1e2fa /doc/sphinx/proof-engine | |
| parent | 259162be000a8a66bf4f551be64d6a5d61edce05 (diff) | |
Mention keywords from g_ltac.mlg used in Ltac.
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index b184311bef..dc994fe863 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -57,6 +57,9 @@ mode but it can also be used in toplevel definitions as shown below. .. note:: + - The grammar reserves the keywords ``lazymatch`` and + ``multimatch`` as well as the token ``||``. + - The infix tacticals ``… || …`` , ``… + …`` , and ``… ; …`` are associative. .. example:: |