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

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