From 20f0e2efb87541e511cf31e220a44e4376c44550 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 2 May 2020 23:22:48 +0200
Subject: Moving lazymatch and multimatch to simple identifiers.

---
 doc/sphinx/proof-engine/ltac.rst | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'doc')

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.
 
-- 
cgit v1.2.3