aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/sphinx/language/gallina-extensions.rst8
1 files changed, 5 insertions, 3 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index f477bf239d..f50cf9340c 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1927,9 +1927,11 @@ Renaming implicit arguments
This command is used to redefine the names of implicit arguments.
-With the assert flag, ``Arguments`` can be used to assert that a given
-object has the expected number of arguments and that these arguments
-are named as expected.
+.. cmd:: Arguments @qualid {* @name} : assert
+ :name: Arguments (assert)
+
+ This command is used to assert that a given object has the expected
+ number of arguments and that these arguments are named as expected.
.. example:: (continued)