From 986bfd1ff69231f1b17efda2fa5d13b88a39caee Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Nov 2019 20:54:52 +0100
Subject: Mention keywords from g_ltac.mlg used in Ltac.

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

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