Deprecate hint declaration/removal with no specified database

Previously, hints added without a specified database where implicitly
put in the "core" database, which was discouraged by the user manual
(because of the lack of modularity of this approach).

4 files changed, 12 insertions, 12 deletions

diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v
index f1095fc9f1..638a4cef21 100644
--- a/plugins/btauto/Algebra.v
+++ b/plugins/btauto/Algebra.v
@@ -10,7 +10,7 @@ end.
 
 Arguments decide P /H.
 
-Hint Extern 5 => progress bool.
+Hint Extern 5 => progress bool : core.
 
 Ltac define t x H :=
 set (x := t) in *; assert (H : t = x) by reflexivity; clearbody x.
@@ -147,7 +147,7 @@ Qed.
 
 (** * The core reflexive part. *)
 
-Hint Constructors valid.
+Hint Constructors valid : core.
 
 Fixpoint beq_poly pl pr :=
 match pl with
@@ -315,7 +315,7 @@ Section Validity.
 
 (* Decision procedure of validity *)
 
-Hint Constructors valid linear.
+Hint Constructors valid linear : core.
 
 Lemma valid_le_compat : forall k l p, valid k p -> (k <= l)%positive -> valid l p.
 Proof.
@@ -425,10 +425,10 @@ match goal with
 | [ |- (?z < Pos.max ?x ?y)%positive ] =>
   apply Pos.max_case_strong; intros; lia
 | _ => zify; omega
-end.
-Hint Resolve Pos.le_max_r Pos.le_max_l.
+end : core.
+Hint Resolve Pos.le_max_r Pos.le_max_l : core.
 
-Hint Constructors valid linear.
+Hint Constructors valid linear : core.
 
 (* Compatibility of validity w.r.t algebraic operations *)
 
diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v
index 4cde08872f..98f5ab067a 100644
--- a/plugins/btauto/Reflect.v
+++ b/plugins/btauto/Reflect.v
@@ -77,10 +77,10 @@ intros var f; induction f; simpl poly_of_formula; simpl formula_eval; auto.
   end.
 Qed.
 
-Hint Extern 5 => change 0 with (min 0 0).
-Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat.
-Local Hint Constructors valid.
-Hint Extern 5 => zify; omega.
+Hint Extern 5 => change 0 with (min 0 0) : core.
+Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat : core.
+Local Hint Constructors valid : core.
+Hint Extern 5 => zify; omega : core.
 
 (* Compatibility with validity *)
 
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index a618fc781f..3a7cf41d43 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -371,7 +371,7 @@ Ltac prop_congr := apply: prop_congr.
 Lemma is_true_true : true.               Proof. by []. Qed.
 Lemma not_false_is_true : ~ false.       Proof. by []. Qed.
 Lemma is_true_locked_true : locked true. Proof. by unlock. Qed.
-Hint Resolve is_true_true not_false_is_true is_true_locked_true.
+Hint Resolve is_true_true not_false_is_true is_true_locked_true : core.
 
 (**  Shorter names.  **)
 Definition isT := is_true_true.
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index e2c0ed7c8b..6535cad8b7 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -398,7 +398,7 @@ End ExtensionalEquality.
 Typeclasses Opaque eqfun.
 Typeclasses Opaque eqrel.
 
-Hint Resolve frefl rrefl.
+Hint Resolve frefl rrefl : core.
 
 Notation "f1 =1 f2" := (eqfun f1 f2)
   (at level 70, no associativity) : fun_scope.