From 259162be000a8a66bf4f551be64d6a5d61edce05 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Nov 2019 18:19:44 +0100
Subject: Mention keywords used in tactics from g_tactic.mlg.

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

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 8989dd29ab..78ac7d00dd 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -36,6 +36,18 @@ language will be described in Chapter :ref:`ltac`.
 Common elements of tactics
 --------------------------
 
+Reserved keywords
+~~~~~~~~~~~~~~~~~
+
+The tactics described in this chapter reserve the following keywords::
+
+  by using
+
+Thus, these keywords cannot be used as identifiers. It also declares
+the following character sequences as tokens::
+
+  ** [= |-
+
 .. _invocation-of-tactics:
 
 Invocation of tactics
-- 
cgit v1.2.3


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(+)

(limited to 'doc/sphinx/proof-engine')

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


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/sphinx/proof-engine')

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