From 4f28dd46d4bfce732693d6904f80e25b53d4fb2a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 15 Nov 2020 17:40:33 +0100 Subject: Document the new warning. --- .../07-commands-and-options/13384-warn-unqualified-hint.rst | 8 ++++++++ doc/sphinx/proofs/automatic-tactics/auto.rst | 7 +++++++ 2 files changed, 15 insertions(+) create mode 100644 doc/changelog/07-commands-and-options/13384-warn-unqualified-hint.rst (limited to 'doc') diff --git a/doc/changelog/07-commands-and-options/13384-warn-unqualified-hint.rst b/doc/changelog/07-commands-and-options/13384-warn-unqualified-hint.rst new file mode 100644 index 0000000000..8ec7198b72 --- /dev/null +++ b/doc/changelog/07-commands-and-options/13384-warn-unqualified-hint.rst @@ -0,0 +1,8 @@ +- **Deprecated:** + The default value for hint locality is currently :attr:`local` in a section and + :attr:`global` otherwise, but is scheduled to change in a future release. For the + time being, adding hints outside of sections without specifying an explicit + locality is therefore triggering a deprecation warning. It is recommended to + use :attr:`export` whenever possible + (`#13384 `_, + by Pierre-Marie Pédrot). diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index 510457fd0c..cc4ab76502 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -289,6 +289,13 @@ automatically created. + :attr:`global` hints are made available by merely requiring the current module. + .. deprecated:: 8.13 + + The default value for hint locality is scheduled to change in a future + release. For the time being, adding hints outside of sections without + specifying an explicit locality is therefore triggering a deprecation + warning. It is recommended to use :attr:`export` whenever possible + The various possible :production:`hint_definition`\s are given below. .. cmdv:: Hint @hint_definition -- cgit v1.2.3