Convert Ltac chapter to prodn

4 files changed, 13 insertions, 13 deletions

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