diff options
Diffstat (limited to 'doc')
6 files changed, 26 insertions, 7 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/changelog/02-specification-language/10997-unsupport-atts-warn.rst b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst new file mode 100644 index 0000000000..43a748b365 --- /dev/null +++ b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst @@ -0,0 +1,3 @@ +- The unsupported attribute error is now an error-by-default warning, + meaning it can be disabled (`#10997 + <https://github.com/coq/coq/pull/10997>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/03-notations/09883-numeral-notations-sorts.rst b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst new file mode 100644 index 0000000000..abc5a516ae --- /dev/null +++ b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst @@ -0,0 +1,4 @@ +- Numeral Notations now support sorts in the input to printing + functions (e.g., numeral notations can be defined for terms + containing things like `@cons Set nat nil`). (`#9883 + <https://github.com/coq/coq/pull/9883>`_, by Jason Gross). 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) diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index ae9d284661..dd65d4aeb3 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1556,6 +1556,11 @@ the following attributes names are recognized: now foo. Abort. +.. warn:: Unsupported attribute + + This warning is an error by default. It is caused by using a + command with some attribute it does not understand. + .. [1] This is similar to the expression “*entry* :math:`\{` sep *entry* :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry* diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index a28ce600ca..02910e603a 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1442,8 +1442,8 @@ Numeral notations of the resulting term will be refreshed. Note that only fully-reduced ground terms (terms containing only - function application, constructors, inductive type families, and - primitive integers) will be considered for printing. + function application, constructors, inductive type families, + sorts, and primitive integers) will be considered for printing. .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). @@ -1592,8 +1592,8 @@ String notations of the resulting term will be refreshed. Note that only fully-reduced ground terms (terms containing only - function application, constructors, inductive type families, and - primitive integers) will be considered for printing. + function application, constructors, inductive type families, + sorts, and primitive integers) will be considered for printing. .. exn:: Cannot interpret this string as a value of type @type |