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

1 files changed, 3 insertions, 0 deletions

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.