Convert Ltac chapter to prodn

8 files changed, 35 insertions, 37 deletions

diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index b2b68482ef..f9d24fde0e 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -34,7 +34,7 @@ The prelude
 This section lists the basic notions and results which are directly
 available in the standard |Coq| system. Most of these constructions
 are defined in the ``Prelude`` module in directory ``theories/Init``
-at the |Coq| root directory; this includes the modules
+in the |Coq| root directory; this includes the modules
 ``Notations``,
 ``Logic``,
 ``Datatypes``,
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
 --------------------------
diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst
index 613669c34b..0ae9fab7ab 100644
--- a/doc/sphinx/language/extensions/arguments-command.rst
+++ b/doc/sphinx/language/extensions/arguments-command.rst
@@ -3,7 +3,7 @@
 Setting properties of a function's arguments
 ++++++++++++++++++++++++++++++++++++++++++++
 
-.. cmd:: Arguments @smart_qualid {* @arg_specs } {* , {* @implicits_alt } } {? : {+, @args_modifier } }
+.. cmd:: Arguments @reference {* @arg_specs } {* , {* @implicits_alt } } {? : {+, @args_modifier } }
    :name: Arguments
 
    .. insertprodn argument_spec args_modifier
@@ -37,7 +37,7 @@ Setting properties of a function's arguments
    extensions into the core language used by the kernel).  The command's effects include:
 
    * Making arguments implicit. Afterward, implicit arguments
-     must be omitted in any expression that applies :token:`smart_qualid`.
+     must be omitted in any expression that applies :token:`reference`.
    * Declaring that some arguments of a given function should
      be interpreted in a given scope.
    * Affecting when the :tacn:`simpl` and :tacn:`cbn` tactics unfold the function.
@@ -82,7 +82,7 @@ Setting properties of a function's arguments
          evaulate to constructors.  See :ref:`Args_effect_on_unfolding`.
 
       :n:`@name {? % @scope }`
-         a *formal parameter* of the function :n:`@smart_qualid` (i.e.
+         a *formal parameter* of the function :n:`@reference` (i.e.
          the parameter name used in the function definition).  Unless `rename` is specified,
          the list of :n:`@name`\s must be a prefix of the formal parameters, including all implicit
          arguments.  `_` can be used to skip over a formal parameter.
@@ -103,15 +103,15 @@ Setting properties of a function's arguments
             :undocumented:
 
       `clear scopes`
-         clears argument scopes of :n:`@smart_qualid`
+         clears argument scopes of :n:`@reference`
       `extra scopes`
          defines extra argument scopes, to be used in case of coercion to ``Funclass``
          (see :ref:`coercions`) or with a computed type.
       `simpl nomatch`
-         prevents performing a simplification step for :n:`@smart_qualid`
+         prevents performing a simplification step for :n:`@reference`
          that would expose a match construct in the head position.  See :ref:`Args_effect_on_unfolding`.
       `simpl never`
-         prevents performing a simplification step for :n:`@smart_qualid`.  See :ref:`Args_effect_on_unfolding`.
+         prevents performing a simplification step for :n:`@reference`.  See :ref:`Args_effect_on_unfolding`.
 
       `clear bidirectionality hint`
          removes the bidirectionality hint, the `&`
@@ -130,7 +130,7 @@ Setting properties of a function's arguments
          .. todo the above feature seems a bit unnatural and doesn't play well with partial
             application.  See https://github.com/coq/coq/pull/11718#discussion_r408841762
 
-   Use :cmd:`About` to view the current implicit arguments setting for a :token:`smart_qualid`.
+   Use :cmd:`About` to view the current implicit arguments setting for a :token:`reference`.
 
    Or use the :cmd:`Print Implicit` command to see the implicit arguments
    of an object (see :ref:`displaying-implicit-args`).
@@ -268,7 +268,7 @@ Binding arguments to a scope
 
          Arguments plus_fct (f1 f2)%F x%R.
 
-   When interpreting a term, if some of the arguments of :token:`smart_qualid` are built
+   When interpreting a term, if some of the arguments of :token:`reference` are built
    from a notation, then this notation is interpreted in the scope stack
    extended by the scope bound (if any) to this argument. The effect of
    the scope is limited to the argument itself. It does not propagate to
diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst
index f55f3c5495..bfda8befff 100644
--- a/doc/sphinx/language/extensions/canonical.rst
+++ b/doc/sphinx/language/extensions/canonical.rst
@@ -27,11 +27,11 @@ applied to an unknown structure instance (an implicit argument) and a
 value. The complete documentation of canonical structures can be found
 in :ref:`canonicalstructures`; here only a simple example is given.
 
-.. cmd:: Canonical {? Structure } @smart_qualid
+.. cmd:: Canonical {? Structure } @reference
          Canonical {? Structure } @ident_decl @def_body
    :name: Canonical Structure; _
 
-   The first form of this command declares an existing :n:`@smart_qualid` as a
+   The first form of this command declares an existing :n:`@reference` as a
    canonical instance of a structure (a record).
 
    The second form defines a new constant as if the :cmd:`Definition` command
@@ -111,7 +111,7 @@ in :ref:`canonicalstructures`; here only a simple example is given.
    It is equivalent to having a :cmd:`Canonical Structure` declaration just
    after the command.
 
-.. cmd:: Print Canonical Projections {* @smart_qualid }
+.. cmd:: Print Canonical Projections {* @reference }
 
    This displays the list of global names that are components of some
    canonical structure. For each of them, the canonical structure of
diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst
index b4f7fe0846..bbd486e3ba 100644
--- a/doc/sphinx/language/extensions/implicit-arguments.rst
+++ b/doc/sphinx/language/extensions/implicit-arguments.rst
@@ -373,7 +373,7 @@ the hiding of implicit arguments for a single function application using the
 Displaying implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Print Implicit @smart_qualid
+.. cmd:: Print Implicit @reference
 
    Displays the implicit arguments associated with an object,
    identifying which arguments are applied maximally or not.
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index 028d0aaf57..b4558ef07f 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -289,7 +289,7 @@ This example emphasizes what the printing settings offer.
 Patterns
 --------
 
-The full syntax of `match` is presented in :ref:`match`.
+The full syntax of `match` is presented in :ref:`match_term`.
 Identifiers in patterns are either constructor names or variables. Any
 identifier that is not the constructor of an inductive or co-inductive
 type is considered to be a variable. A variable name cannot occur more