Keywords: Applying suggestions from Jim Fehrle and Théo Zimmermann.

2 files changed, 23 insertions, 16 deletions

diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index acdd4408ed..899173a83a 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -9,11 +9,11 @@ The |Coq| library
 
 The |Coq| library has two parts:
 
-  * **The basic library**: definitions and theorems for
+  * The :gdef:`prelude`: definitions and theorems for
     the most commonly used elementary logical notions and
     data types. |Coq| normally loads these files automatically when it starts.
 
-  * **The standard library**: general-purpose libraries with
+  * The :gdef:`standard library`: general-purpose libraries with
     definitions and theorems for sets, lists, sorting,
     arithmetic, etc. To use these files, users must load them explicitly
     with the ``Require`` command (see :ref:`compiled-files`)
@@ -28,8 +28,8 @@ also be browsed at http://coq.inria.fr/stdlib/.
 
 
 
-The basic library
------------------
+The prelude
+-----------
 
 This section lists the basic notions and results which are directly
 available in the standard |Coq| system. Most of these constructions
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,