From 62f6fb862ce4f3eec46200d11e503aa5d6d051db Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Nov 2019 17:18:06 +0100
Subject: Documenting plugin/tactic/stdlib keywords in corresponding chapters.

Incidentally removing "discriminated", "(bfs)" and "(dfs)" from
keywords. It is enough to make them normal identifiers.

Note:
- keywords reserved by the tactics are: ** [= _eqn |- by using
- keywords reserved by ltac are: lazymatch multimatch ||
---
 doc/sphinx/language/core/basic.rst | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'doc/sphinx/language/core/basic.rst')

diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 9473cc5a15..3940242bb3 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -134,7 +134,7 @@ Keywords
   used as identifiers::
 
     _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop
-    SProp Set Theorem Type Variable as at cofix discriminated else end
+    SProp Set Theorem Type Variable as at cofix else end
     fix for forall fun if in let match return then where with
 
   Note that notations and plugins may define additional keywords.
@@ -150,10 +150,10 @@ Other tokens
   Here are the character sequences that |Coq| directly defines as tokens
   without using :cmd:`Notation`::
 
-    ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - ->
+    ! #[ % & ' ( () ) * + , - ->
     . .( .. ... / : ::= := :> :>> ; < <+ <- <:
-    <<: <= = => > >-> >= ? @ @{ [ [= ] _
-    `( `{ { {| | |- || }
+    <<: <= = => > >-> >= ? @ @{ [ ] _
+    `( `{ { {| | }
 
   When multiple tokens match the beginning of a sequence of characters,
   the longest matching token is used.
-- 
cgit v1.2.3


From 037c8d299ca1a5aef9813133dca07ad6f35e1e75 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 6 May 2020 16:59:19 +0200
Subject: Keywords: Applying suggestions from Jim Fehrle and Théo Zimmermann.

---
 doc/sphinx/language/core/basic.rst | 31 +++++++++++++++++++------------
 1 file changed, 19 insertions(+), 12 deletions(-)

(limited to 'doc/sphinx/language/core/basic.rst')

diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 3940242bb3..aa93b4d21f 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -130,31 +130,38 @@ Strings
   identified with :production:`string`.
 
 Keywords
-  The following character sequences are reserved keywords that cannot be
-  used as identifiers::
+  The following character sequences are keywords defined in the main Coq grammar
+  that cannot be used as identifiers (even when starting Coq with the `-noinit`
+  command-line flag)::
 
     _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop
     SProp Set Theorem Type Variable as at cofix else end
     fix for forall fun if in let match return then where with
 
-  Note that notations and plugins may define additional keywords.
+  The following are keywords defined in notations or plugins loaded in the :term:`prelude`::
 
-Other tokens
-  The set of
-  tokens defined at any given time can vary because the :cmd:`Notation`
-  command can define new tokens.  A :cmd:`Require` command may load more notation definitions,
-  while the end of a :cmd:`Section` may remove notations.  Some notations
-  are defined in the standard library (see :ref:`thecoqlibrary`) and are generally
-  loaded automatically at startup time.
+    IF by exists exists2 using
+
+  Note that loading additional modules or plugins may expand the set of reserved
+  keywords.
 
-  Here are the character sequences that |Coq| directly defines as tokens
-  without using :cmd:`Notation`::
+Other tokens
+  The following character sequences are tokens defined in the main Coq grammar
+  (even when starting Coq with the `-noinit` command-line flag)::
 
     ! #[ % & ' ( () ) * + , - ->
     . .( .. ... / : ::= := :> :>> ; < <+ <- <:
     <<: <= = => > >-> >= ? @ @{ [ ] _
     `( `{ { {| | }
 
+  The following character sequences are tokens defined in notations or plugins
+  loaded in the :term:`prelude`::
+
+    ** [= |- || ->
+
+  Note that loading additional modules or plugins may expand the set of defined
+  tokens.
+
   When multiple tokens match the beginning of a sequence of characters,
   the longest matching token is used.
   Occasionally you may need to insert spaces to separate tokens.  For example,
-- 
cgit v1.2.3