Merge PR #12103: Convert Ltac chapter to prodn

3 files changed, 21 insertions, 23 deletions

diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 8918e87180..d7f7259ab0 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -57,7 +57,7 @@ appending the level to the nonterminal name (as in :n:`@term100` or
 
    |Coq| uses an extensible parser.  Plugins and the :ref:`notation
    system <syntax-extensions-and-notation-scopes>` can extend the
-   syntax at run time.  Some notations are defined in the prelude,
+   syntax at run time.  Some notations are defined in the :term:`prelude`,
    which is loaded by default.  The documented grammar doesn't include
    these notations.  Precedence levels not used by the base grammar
    are omitted from the documentation, even though they could still be
@@ -119,21 +119,19 @@ Numerals
   integer.  Underscores embedded in the digits are ignored, for example
   ``1_000_000`` is the same as ``1000000``.
 
-  .. insertprodn numeral digit
+  .. insertprodn numeral hexdigit
 
   .. prodn::
-     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 ::= {| + | - }
+     numeral ::= {? - } @decnum {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnum }
+     | {? - } @hexnum {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnum }
      int ::= {? - } @num
-     decimal ::= @decnum {? . {+ @digitu } } {? {| e | E } {? @sign } @decnum }
-     hexadecimal ::= @hexnum {? . {+ @hexdigitu } } {? {| p | P } {? @sign } @decnum }
-     numeral ::= {? - } {| @decimal | @hexadecimal }
+     num ::= {| @decnum | @hexnum }
+     decnum ::= @digit {* {| @digit | _ } }
+     digit ::= 0 .. 9
+     hexnum ::= {| 0x | 0X } @hexdigit {* {| @hexdigit | _ } }
+     hexdigit ::= {| 0 .. 9 | a .. f | A .. F }
+
+  .. todo PR need some code fixes for hex, see PR 11948
 
 Strings
   Strings begin and end with ``"`` (double quote).  Use ``""`` to represent
@@ -294,7 +292,7 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types
         document ::= {* @sentence }
         sentence ::= {? @attributes } @command .
         | {? @attributes } {? @num : } @query_command .
-        | {? @attributes } {? @toplevel_selector } @ltac_expr {| . | ... }
+        | {? @attributes } {? @toplevel_selector : } @ltac_expr {| . | ... }
         | @control_command
 
      :n:`@ltac_expr` syntax supports both simple and compound
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 0e637e5aa3..42203d9d65 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -34,18 +34,18 @@ Type cast
 .. insertprodn term_cast term_cast
 
 .. prodn::
-   term_cast ::= @term10 <: @term
-   | @term10 <<: @term
-   | @term10 : @term
+   term_cast ::= @term10 <: @type
+   | @term10 <<: @type
+   | @term10 : @type
    | @term10 :>
 
-The expression :n:`@term : @type` is a type cast expression. It enforces
-the type of :n:`@term` to be :n:`@type`.
+The expression :n:`@term10 : @type` is a type cast expression. It enforces
+the type of :n:`@term10` to be :n:`@type`.
 
-:n:`@term <: @type` locally sets up the virtual machine for checking that
-:n:`@term` has type :n:`@type`.
+:n:`@term10 <: @type` locally sets up the virtual machine for checking that
+:n:`@term10` has type :n:`@type`.
 
-:n:`@term <<: @type` uses native compilation for checking that :n:`@term`
+:n:`@term10 <<: @type` uses native compilation for checking that :n:`@term10`
 has type :n:`@type`.
 
 .. _gallina-definitions:
diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst
index 6d4676b3c4..d00a2f4100 100644
--- a/doc/sphinx/language/core/variants.rst
+++ b/doc/sphinx/language/core/variants.rst
@@ -52,7 +52,7 @@ Private (matching) inductive types
 
 .. index:: match ... with ...
 
-.. _match:
+.. _match_term:
 
 Definition by cases: match
 --------------------------