diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/02-specification-language/10985-about-arguments.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 8 |
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) |