1 files changed, 37 insertions, 21 deletions

diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 9473cc5a15..250a0f0326 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -111,18 +111,27 @@ Identifiers
 
 Numerals
   Numerals are sequences of digits with an optional fractional part
-  and exponent, optionally preceded by a minus sign. :n:`@int` is an integer;
-  a numeral without fractional or exponent parts. :n:`@num` is a non-negative
+  and exponent, optionally preceded by a minus sign. Hexadecimal numerals
+  start with ``0x`` or ``0X``. :n:`@int` is an integer;
+  a numeral without fractional nor exponent parts. :n:`@num` is a non-negative
   integer.  Underscores embedded in the digits are ignored, for example
   ``1_000_000`` is the same as ``1000000``.
 
   .. insertprodn numeral digit
 
   .. prodn::
-     numeral ::= {+ @digit } {? . {+ @digit } } {? {| e | E } {? {| + | - } } {+ @digit } }
-     int ::= {? - } {+ @digit }
-     num ::= {+ @digit }
      digit ::= 0 .. 9
+     digitu ::= {| @digit | _ }
+     hexdigit ::= {| 0 .. 9 | a..f | A..F }
+     hexdigitu ::= {| @hexdigit | _ }
+     decnum ::= @digit {* @digitu }
+     hexnum ::= {| 0x | 0X } @hexdigit {* @hexdigitu }
+     num ::= {| @decnum | @hexnum }
+     sign ::= {| + | - }
+     int ::= {? - } @num
+     decimal ::= @decnum {? . {+ @digitu } } {? {| e | E } {? @sign } @decnum }
+     hexadecimal ::= @hexnum {? . {+ @hexdigitu } } {? {| p | P } {? @sign } @decnum }
+     numeral ::= {? - } {| @decimal | @hexadecimal }
 
 Strings
   Strings begin and end with ``"`` (double quote).  Use ``""`` to represent
@@ -130,30 +139,37 @@ 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 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.
+  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)::
 
-    ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - ->
+    ! #[ % & ' ( () ) * + , - ->
     . .( .. ... / : ::= := :> :>> ; < <+ <- <:
-    <<: <= = => > >-> >= ? @ @{ [ [= ] _
-    `( `{ { {| | |- || }
+    <<: <= = => > >-> >= ? @ @{ [ ] _
+    `( `{ { {| | }
+
+  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.