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/02-specification-language/11368-trailing_implicit_error.rst | |
| parent | 51a938a260d989f11fb1cd1d7a0205c6183f3809 (diff) | |
Convert syntax extensions chapter to prodn
Diffstat (limited to 'doc/changelog/02-specification-language/11368-trailing_implicit_error.rst')
| -rw-r--r-- | doc/changelog/02-specification-language/11368-trailing_implicit_error.rst | 2 |
1 files changed, 1 insertions, 1 deletions
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>`_, |