From 3d2164ab0681d65d04bd0ba161369faa7ff5f63d Mon Sep 17 00:00:00 2001 From: SimonBoulier Date: Tue, 7 Jan 2020 11:34:22 +0100 Subject: Trailing implicit error: changelog --- .../02-specification-language/11368-trailing_implicit_error.rst | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 doc/changelog/02-specification-language/11368-trailing_implicit_error.rst diff --git a/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst new file mode 100644 index 0000000000..9a8d619f3b --- /dev/null +++ b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst @@ -0,0 +1,6 @@ +- **Changed:** + The warning raised when a trailing implicit is declared to be non maximally + inserted (with the command `Arguments`) has been turned into an error. + This was deprecated since Coq 8.10. + (`#11368 `_, + by SimonBoulier). -- cgit v1.2.3