diff options
| author | Jim Fehrle | 2020-02-29 12:27:51 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2020-04-26 22:19:01 -0700 |
| commit | a7f56cb5799bc830285f4acf96678486a5929172 (patch) | |
| tree | 12c83204413ad08255400b3e35c508e6815cd9c0 /doc/changelog | |
| parent | 51a938a260d989f11fb1cd1d7a0205c6183f3809 (diff) | |
Convert syntax extensions chapter to prodn
Diffstat (limited to 'doc/changelog')
3 files changed, 3 insertions, 3 deletions
diff --git a/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst index 67e43973ce..768ef68339 100644 --- a/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst +++ b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst @@ -1,5 +1,5 @@ - **Added:** - Syntax for non maximal implicit arguments in definitions and terms using + Syntax for non-maximal implicit arguments in definitions and terms using square brackets. The syntax is ``[x : A]``, ``[x]``, ```[A]`` to be consistent with the command :cmd:`Arguments`. (`#11235 <https://github.com/coq/coq/pull/11235>`_, diff --git a/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst index 11d7218ed0..66139f76e1 100644 --- a/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst +++ b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst @@ -1,5 +1,5 @@ - **Changed:** - The warning raised when a trailing implicit is declared to be non maximally + The warning raised when a trailing implicit is declared to be non-maximally inserted (with the command :cmd:`Arguments`) has been turned into an error. This was deprecated since Coq 8.10 (`#11368 <https://github.com/coq/coq/pull/11368>`_, diff --git a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst index d95f554766..eeb4c755f6 100644 --- a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst +++ b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst @@ -10,7 +10,7 @@ Herbelin, fixing `#4690 <https://github.com/coq/coq/pull/4690>`_ and `#11091 <https://github.com/coq/coq/pull/11091>`_). -- **Changed:** Interpretation scopes are now always inherited in +- **Changed:** Notation scopes are now always inherited in notations binding a partially applied constant, including for notations binding an expression of the form :n:`@@qualid`. The latter was not the case beforehand |