Merge PR #8987: Deprecate hint declaration/removal with no specified database

1 files changed, 19 insertions, 4 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 08aee9533f..0405e4f27c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1098,13 +1098,28 @@ let vernac_restore_state file =
 let vernac_create_hintdb ~module_local id b =
   Hints.create_hint_db module_local id full_transparent_state b
 
-let vernac_remove_hints ~module_local dbs ids =
-  Hints.remove_hints module_local dbs (List.map Smartlocate.global_with_alias ids)
+let warn_implicit_core_hint_db =
+  CWarnings.create ~name:"implicit-core-hint-db" ~category:"deprecated"
+         (fun () -> strbrk "Adding and removing hints in the core database implicitly is deprecated. "
+             ++ strbrk"Please specify a hint database.")
+
+let vernac_remove_hints ~module_local dbnames ids =
+  let dbnames =
+    if List.is_empty dbnames then
+      (warn_implicit_core_hint_db (); ["core"])
+    else dbnames
+  in
+  Hints.remove_hints module_local dbnames (List.map Smartlocate.global_with_alias ids)
 
-let vernac_hints ~atts lb h =
+let vernac_hints ~atts dbnames h =
+  let dbnames =
+    if List.is_empty dbnames then
+      (warn_implicit_core_hint_db (); ["core"])
+    else dbnames
+  in
   let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
   let local = enforce_module_locality local in
-  Hints.add_hints ~local lb (Hints.interp_hints poly h)
+  Hints.add_hints ~local dbnames (Hints.interp_hints poly h)
 
 let vernac_syntactic_definition ~module_local lid x y =
   Dumpglob.dump_definition lid false "syndef";