Document the new warning.

1 files changed, 8 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).