From bc4f73821733365fb5882f455ca503feaa96f11f Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Thu, 16 May 2019 16:47:35 -0400
Subject: [refman] Give explicit names to the various 'Arguments' commands

---
 doc/sphinx/language/gallina-extensions.rst | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'doc/sphinx/language')

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.
 
-- 
cgit v1.2.3