Document the new warning.

2 files changed, 15 insertions, 0 deletions

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 <https://github.com/coq/coq/pull/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