[refman] Give explicit names to the various 'Arguments' commands

5 files changed, 9 insertions, 6 deletions

diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 701c62cdce..db4ebd5e38 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -656,8 +656,8 @@ changes:
     attribute.
 
   - Removed deprecated commands ``Arguments Scope`` and ``Implicit
-    Arguments`` in favor of :cmd:`Arguments`, with the help of Jasper
-    Hugunin.
+    Arguments`` in favor of :cmd:`Arguments (scopes)` and
+    :cmd:`Arguments (implicits)`, with the help of Jasper Hugunin.
 
   - New flag :flag:`Uniform Inductive Parameters` by Jasper Hugunin to
     avoid repeating uniform parameters in constructor declarations.
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index c48964d66c..2b673ff62b 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1662,6 +1662,7 @@ Declaring Implicit Arguments
    of :token:`qualid`.
 
 .. cmd:: Arguments @qualid : clear implicits
+   :name: Arguments (clear implicits)
 
    This command clears implicit arguments.
 
@@ -1738,6 +1739,7 @@ Automatic declaration of implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. cmd:: Arguments @qualid : default implicits
+   :name: Arguments (default implicits)
 
    This command tells |Coq| to automatically detect what are the implicit arguments of a
    defined object.
@@ -1908,6 +1910,7 @@ Renaming implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. cmd:: Arguments @qualid {* @name} : @rename
+   :name: Arguments (rename)
 
    This command is used to redefine the names of implicit arguments.
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 2ee23df019..cd023eb1b1 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3159,7 +3159,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
    + A constant can be marked to be unfolded only if applied to enough
      arguments. The number of arguments required can be specified using the
-     ``/`` symbol in the argument list of the :cmd:`Arguments` vernacular command.
+     ``/`` symbol in the argument list of the :cmd:`Arguments <Arguments (implicits)>` vernacular command.
 
      .. example::
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 26dc4e02cf..fa5ca81a7c 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1208,7 +1208,7 @@ Controlling the locality of commands
      effect of the command to the current module if the command does not occur in a
      section and the Global modifier extends the effect outside the current
      sections and current module if the command occurs in a section. As an example,
-     the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong
+     the :cmd:`Arguments <Arguments (implicits)>`, :cmd:`Ltac` or :cmd:`Notation` commands belong
      to this category. Notice that a subclass of these commands do not support
      extension of their scope outside sections at all and the Global modifier is not
      applicable to them.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 6da42f4a48..6a681d83f0 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1143,8 +1143,8 @@ Binding types of arguments to an interpretation scope
    scope of operations on the natural numbers), it may be convenient to bind it
    to this type. When a scope ``scope`` is bound to a type ``type``, any new function
    defined later on gets its arguments of type ``type`` interpreted by default in
-   scope scope (this default behavior can however be overwritten by explicitly
-   using the command :cmd:`Arguments`).
+   scope ``scope`` (this default behavior can however be overwritten by explicitly
+   using the command :cmd:`Arguments <Arguments (scopes)>`).
 
    Whether the argument of a function has some type ``type`` is determined
    statically. For instance, if ``f`` is a polymorphic function of type