Merge PR #10985: Print argument info as an Arguments command in About

Ack-by: Zimmi48
Ack-by: cpitclaudel
Reviewed-by: ejgallego

2 files changed, 10 insertions, 3 deletions

diff --git a/doc/changelog/02-specification-language/10985-about-arguments.rst b/doc/changelog/02-specification-language/10985-about-arguments.rst
new file mode 100644
index 0000000000..1e05b0b0fe
--- /dev/null
+++ b/doc/changelog/02-specification-language/10985-about-arguments.rst
@@ -0,0 +1,5 @@
+- The output of the :cmd:`Print` and :cmd:`About` commands has
+  changed. Arguments meta-data is now displayed as the corresponding
+  :cmd:`Arguments <Arguments (implicits)>` command instead of the
+  human-targeted prose used in previous Coq versions. (`#10985
+  <https://github.com/coq/coq/pull/10985>`_, by Gaëtan Gilbert).
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)