From 3fe5f962d236448e78f55dd6761da173a30f8be4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 15 Nov 2020 13:38:41 +0100
Subject: Tentative fix for the refman.

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

(limited to 'doc')

diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst
index 485b92342d..510457fd0c 100644
--- a/doc/sphinx/proofs/automatic-tactics/auto.rst
+++ b/doc/sphinx/proofs/automatic-tactics/auto.rst
@@ -123,6 +123,10 @@ Programmable proof search
 
    .. example::
 
+      .. coqtop:: none
+
+         Set Warnings "-deprecated-hint-without-locality".
+
       .. coqtop:: all
 
          Hint Resolve ex_intro : core.
@@ -405,6 +409,10 @@ automatically created.
 
       .. example::
 
+         .. coqtop:: none
+
+            Set Warnings "-deprecated-hint-without-locality".
+
          .. coqtop:: in
 
             Hint Extern 4 (~(_ = _)) => discriminate : core.
@@ -419,7 +427,11 @@ automatically created.
 
       .. example::
 
-         .. coqtop:: reset all
+         .. coqtop:: reset none
+
+            Set Warnings "-deprecated-hint-without-locality".
+
+         .. coqtop:: all
 
             Require Import List.
             Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize  X1, X2; decide equality : eqdec.
-- 
cgit v1.2.3


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 <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
-- 
cgit v1.2.3