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

2 files changed, 2 insertions, 2 deletions

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.