diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index dc994fe863..90173d65bf 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -57,8 +57,7 @@ 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 grammar reserves the token ``||``. - The infix tacticals ``… || …`` , ``… + …`` , and ``… ; …`` are associative. |