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.

---
 doc/sphinx/proofs/automatic-tactics/auto.rst | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'doc/sphinx/proofs')

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