From 7daf04e53bdee6b0c9d0171c1e0d05903d677d3a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 13 Nov 2020 19:42:54 +0100
Subject: Warning on hint commands that have no explicit locality.

---
 vernac/vernacentries.ml | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 761f6ef5b7..4e52af7959 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1314,6 +1314,14 @@ let warn_implicit_core_hint_db =
          (fun () -> strbrk "Adding and removing hints in the core database implicitly is deprecated. "
              ++ strbrk"Please specify a hint database.")
 
+let warn_deprecated_hint_without_locality =
+  CWarnings.create ~name:"deprecated-hint-without-locality" ~category:"deprecated"
+    (fun () -> strbrk "The default value for hint locality is currently \
+    \"local\" in a section and \"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 deprecated. It is \
+    recommended to use \"export\" whenever possible.")
+
 let check_hint_locality = function
 | OptGlobal ->
   if Global.sections_are_opened () then
@@ -1323,7 +1331,10 @@ let check_hint_locality = function
   if Global.sections_are_opened () then
   CErrors.user_err Pp.(str
     "This command does not support the export attribute in sections.");
-| OptDefault | OptLocal -> ()
+| OptDefault ->
+  if not @@ Global.sections_are_opened () then
+    warn_deprecated_hint_without_locality ()
+| OptLocal -> ()
 
 let vernac_remove_hints ~atts dbnames ids =
   let locality = Attributes.(parse option_locality atts) in
-- 
cgit v1.2.3