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 (limited to 'doc') 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 From bb22f188b46527fb5829562edc946b743b326309 Mon Sep 17 00:00:00 2001 From: SimonBoulier Date: Tue, 7 Jan 2020 11:34:31 +0100 Subject: Trailing implicit error: documentation --- doc/sphinx/language/gallina-extensions.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 78428be18f..6be501199d 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1728,11 +1728,11 @@ Declaring Implicit Arguments To know which are the implicit arguments of an object, use the command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`). -.. warn:: Argument number @num is a trailing implicit so must be maximal. +.. exn:: Argument id is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. For instance in - .. coqtop:: all warn + .. coqtop:: all fail Arguments prod _ [_]. -- cgit v1.2.3 From 9cbd740cd7e8936a9411528fc5dd4d5ddb0d3c1d Mon Sep 17 00:00:00 2001 From: SimonBoulier Date: Wed, 8 Jan 2020 10:20:20 +0100 Subject: Trailing implicit: Maxime's suggestions --- doc/sphinx/language/gallina-extensions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 6be501199d..d85be0646a 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1728,7 +1728,7 @@ Declaring Implicit Arguments To know which are the implicit arguments of an object, use the command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`). -.. exn:: Argument id is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. +.. exn:: Argument @ident is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. For instance in -- cgit v1.2.3 From b9f3e03dd07e678ce900f332cf4653c5d222ee16 Mon Sep 17 00:00:00 2001 From: SimonBoulier Date: Wed, 8 Jan 2020 11:00:05 +0100 Subject: Update doc/changelog/02-specification-language/11368-trailing_implicit_error.rst Co-Authored-By: Théo Zimmermann --- .../02-specification-language/11368-trailing_implicit_error.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') 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 9a8d619f3b..a7ffde31fc 100644 --- a/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst +++ b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst @@ -1,6 +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. + inserted (with the command cmd:`Arguments `) has been turned into an error. This was deprecated since Coq 8.10. (`#11368 `_, by SimonBoulier). -- cgit v1.2.3