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

6 files changed, 64 insertions, 64 deletions

diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v
index 24333ad815..f82ca5fa3c 100644
--- a/theories/Structures/DecidableType.v
+++ b/theories/Structures/DecidableType.v
@@ -38,8 +38,8 @@ Module KeyDecidableType(D:DecidableType).
   Definition eqke (p p':key*elt) :=
           eq (fst p) (fst p') /\ (snd p) = (snd p').
 
-  Hint Unfold eqk eqke.
-  Hint Extern 2 (eqke ?a ?b) => split.
+  Hint Unfold eqk eqke : core.
+  Hint Extern 2 (eqke ?a ?b) => split : core.
 
    (* eqke is stricter than eqk *)
 
@@ -70,8 +70,8 @@ Module KeyDecidableType(D:DecidableType).
     unfold eqke; intuition; [ eauto | congruence ].
   Qed.
 
-  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
-  Hint Immediate eqk_sym eqke_sym.
+  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core.
+  Hint Immediate eqk_sym eqke_sym : core.
 
   Global Instance eqk_equiv : Equivalence eqk.
   Proof. split; eauto. Qed.
@@ -84,7 +84,7 @@ Module KeyDecidableType(D:DecidableType).
   Proof.
     unfold eqke; induction 1; intuition. 
   Qed.
-  Hint Resolve InA_eqke_eqk.
+  Hint Resolve InA_eqke_eqk : core.
 
   Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
   Proof.
@@ -94,7 +94,7 @@ Module KeyDecidableType(D:DecidableType).
   Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
   Definition In k m := exists e:elt, MapsTo k e m.
 
-  Hint Unfold MapsTo In.
+  Hint Unfold MapsTo In : core.
 
   (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
 
@@ -140,13 +140,13 @@ Module KeyDecidableType(D:DecidableType).
 
  End Elt.
 
- Hint Unfold eqk eqke.
- Hint Extern 2 (eqke ?a ?b) => split.
- Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
- Hint Immediate eqk_sym eqke_sym.
- Hint Resolve InA_eqke_eqk.
- Hint Unfold MapsTo In.
- Hint Resolve In_inv_2 In_inv_3.
+ Hint Unfold eqk eqke : core.
+ Hint Extern 2 (eqke ?a ?b) => split : core.
+ Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core.
+ Hint Immediate eqk_sym eqke_sym : core.
+ Hint Resolve InA_eqke_eqk : core.
+ Hint Unfold MapsTo In : core.
+ Hint Resolve In_inv_2 In_inv_3 : core.
 
 End KeyDecidableType.
 
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index 5f60a979c6..4143dba547 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -53,8 +53,8 @@ Module Type IsEqOrig (Import E:Eq').
   Axiom eq_refl : forall x : t, x==x.
   Axiom eq_sym : forall x y : t, x==y -> y==x.
   Axiom eq_trans : forall x y z : t, x==y -> y==z -> x==z.
-  Hint Immediate eq_sym.
-  Hint Resolve eq_refl eq_trans.
+  Hint Immediate eq_sym : core.
+  Hint Resolve eq_refl eq_trans : core.
 End IsEqOrig.
 
 (** * Types with decidable equality *)
diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v
index 7b6ee2eaca..c738b57f44 100644
--- a/theories/Structures/EqualitiesFacts.v
+++ b/theories/Structures/EqualitiesFacts.v
@@ -22,7 +22,7 @@ Module KeyDecidableType(D:DecidableType).
  Definition eqk {elt} : relation (key*elt) := D.eq @@1.
  Definition eqke {elt} : relation (key*elt) := D.eq * Logic.eq.
 
- Hint Unfold eqk eqke.
+ Hint Unfold eqk eqke : core.
 
  (** eqk, eqke are equalities *)
 
@@ -60,7 +60,7 @@ Module KeyDecidableType(D:DecidableType).
  Lemma eqk_1 {elt} k k' (e e':elt) : eqk (k,e) (k',e') -> D.eq k k'.
  Proof. trivial. Qed.
 
- Hint Resolve eqke_1 eqke_2 eqk_1.
+ Hint Resolve eqke_1 eqke_2 eqk_1 : core.
 
  (* Additional facts *)
 
@@ -69,7 +69,7 @@ Module KeyDecidableType(D:DecidableType).
  Proof.
   induction 1; firstorder.
  Qed.
- Hint Resolve InA_eqke_eqk.
+ Hint Resolve InA_eqke_eqk : core.
 
  Lemma InA_eqk_eqke {elt} p (m:list (key*elt)) :
   InA eqk p m -> exists q, eqk p q /\ InA eqke q m.
@@ -86,7 +86,7 @@ Module KeyDecidableType(D:DecidableType).
  Definition MapsTo {elt} (k:key)(e:elt):= InA eqke (k,e).
  Definition In {elt} k m := exists e:elt, MapsTo k e m.
 
- Hint Unfold MapsTo In.
+ Hint Unfold MapsTo In : core.
 
  (* Alternative formulations for [In k l] *)
 
@@ -167,9 +167,9 @@ Module KeyDecidableType(D:DecidableType).
   eauto with *.
  Qed.
 
- Hint Extern 2 (eqke ?a ?b) => split.
- Hint Resolve InA_eqke_eqk.
- Hint Resolve In_inv_2 In_inv_3.
+ Hint Extern 2 (eqke ?a ?b) => split : core.
+ Hint Resolve InA_eqke_eqk : core.
+ Hint Resolve In_inv_2 In_inv_3 : core.
 
 End KeyDecidableType.
 
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index f6fc247d5a..d000b75bf4 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -42,8 +42,8 @@ Module Type MiniOrderedType.
 
   Parameter compare : forall x y : t, Compare lt eq x y.
 
-  Hint Immediate eq_sym.
-  Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.
+  Hint Immediate eq_sym : core.
+  Hint Resolve eq_refl eq_trans lt_not_eq lt_trans : core.
 
 End MiniOrderedType.
 
@@ -143,9 +143,9 @@ Module OrderedTypeFacts (Import O: OrderedType).
   Lemma eq_not_gt x y : eq x y -> ~ lt y x. Proof. order. Qed.
   Lemma lt_not_gt x y : lt x y -> ~ lt y x. Proof. order. Qed.
 
-  Hint Resolve gt_not_eq eq_not_lt.
-  Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq.
-  Hint Resolve eq_not_gt lt_antirefl lt_not_gt.
+  Hint Resolve gt_not_eq eq_not_lt : core.
+  Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq : core.
+  Hint Resolve eq_not_gt lt_antirefl lt_not_gt : core.
 
   Lemma elim_compare_eq :
    forall x y : t,
@@ -247,8 +247,8 @@ Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat). Qed.
 
 End ForNotations.
 
-Hint Resolve ListIn_In Sort_NoDup Inf_lt.
-Hint Immediate In_eq Inf_lt.
+Hint Resolve ListIn_In Sort_NoDup Inf_lt : core.
+Hint Immediate In_eq Inf_lt : core.
 
 End OrderedTypeFacts.
 
@@ -266,8 +266,8 @@ Module KeyOrderedType(O:OrderedType).
           eq (fst p) (fst p') /\ (snd p) = (snd p').
   Definition ltk (p p':key*elt) := lt (fst p) (fst p').
 
-  Hint Unfold eqk eqke ltk.
-  Hint Extern 2 (eqke ?a ?b) => split.
+  Hint Unfold eqk eqke ltk : core.
+  Hint Extern 2 (eqke ?a ?b) => split : core.
 
    (* eqke is stricter than eqk *)
 
@@ -283,7 +283,7 @@ Module KeyOrderedType(O:OrderedType).
 
    Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x.
    Proof. auto. Qed.
-   Hint Immediate ltk_right_r ltk_right_l.
+   Hint Immediate ltk_right_r ltk_right_l : core.
 
   (* eqk, eqke are equalities, ltk is a strict order *)
 
@@ -319,9 +319,9 @@ Module KeyOrderedType(O:OrderedType).
     exact (lt_not_eq H H1).
   Qed.
 
-  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
-  Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke.
-  Hint Immediate eqk_sym eqke_sym.
+  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core.
+  Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : core.
+  Hint Immediate eqk_sym eqke_sym : core.
 
   Global Instance eqk_equiv : Equivalence eqk.
   Proof. constructor; eauto. Qed.
@@ -359,22 +359,22 @@ Module KeyOrderedType(O:OrderedType).
       intros (k,e) (k',e') (k'',e'').
       unfold ltk, eqk; simpl; eauto.
   Qed.
-  Hint Resolve eqk_not_ltk.
-  Hint Immediate ltk_eqk eqk_ltk.
+  Hint Resolve eqk_not_ltk : core.
+  Hint Immediate ltk_eqk eqk_ltk : core.
 
   Lemma InA_eqke_eqk :
      forall x m, InA eqke x m -> InA eqk x m.
   Proof.
     unfold eqke; induction 1; intuition.
   Qed.
-  Hint Resolve InA_eqke_eqk.
+  Hint Resolve InA_eqke_eqk : core.
 
   Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
   Definition In k m := exists e:elt, MapsTo k e m.
   Notation Sort := (sort ltk).
   Notation Inf := (lelistA ltk).
 
-  Hint Unfold MapsTo In.
+  Hint Unfold MapsTo In : core.
 
   (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
 
@@ -405,8 +405,8 @@ Module KeyOrderedType(O:OrderedType).
   Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.
   Proof. exact (InfA_ltA ltk_strorder). Qed.
 
-  Hint Immediate Inf_eq.
-  Hint Resolve Inf_lt.
+  Hint Immediate Inf_eq : core.
+  Hint Resolve Inf_lt : core.
 
   Lemma Sort_Inf_In :
       forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p.
@@ -469,19 +469,19 @@ Module KeyOrderedType(O:OrderedType).
 
  End Elt.
 
- Hint Unfold eqk eqke ltk.
- Hint Extern 2 (eqke ?a ?b) => split.
- Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
- Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke.
- Hint Immediate eqk_sym eqke_sym.
- Hint Resolve eqk_not_ltk.
- Hint Immediate ltk_eqk eqk_ltk.
- Hint Resolve InA_eqke_eqk.
- Hint Unfold MapsTo In.
- Hint Immediate Inf_eq.
- Hint Resolve Inf_lt.
- Hint Resolve Sort_Inf_NotIn.
- Hint Resolve In_inv_2 In_inv_3.
+ Hint Unfold eqk eqke ltk : core.
+ Hint Extern 2 (eqke ?a ?b) => split : core.
+ Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core.
+ Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : core.
+ Hint Immediate eqk_sym eqke_sym : core.
+ Hint Resolve eqk_not_ltk : core.
+ Hint Immediate ltk_eqk eqk_ltk : core.
+ Hint Resolve InA_eqke_eqk : core.
+ Hint Unfold MapsTo In : core.
+ Hint Immediate Inf_eq : core.
+ Hint Resolve Inf_lt : core.
+ Hint Resolve Sort_Inf_NotIn : core.
+ Hint Resolve In_inv_2 In_inv_3 : core.
 
 End KeyOrderedType.
 
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index 42756ad339..310a22a0a4 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -181,7 +181,7 @@ Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder
     we coerce [bool] into [Prop]. *)
 
 Local Coercion is_true : bool >-> Sortclass.
-Hint Unfold is_true.
+Hint Unfold is_true : core.
 
 Module Type HasLeb (Import T:Typ).
  Parameter Inline leb : t -> t -> bool.
diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v
index abdb9eff05..fef9b14a9e 100644
--- a/theories/Structures/OrdersLists.v
+++ b/theories/Structures/OrdersLists.v
@@ -50,8 +50,8 @@ Proof. exact (InfA_alt O.eq_equiv O.lt_strorder O.lt_compat). Qed.
 Lemma Sort_NoDup : forall l, Sort l -> NoDup l.
 Proof. exact (SortA_NoDupA O.eq_equiv O.lt_strorder O.lt_compat) . Qed.
 
-Hint Resolve ListIn_In Sort_NoDup Inf_lt.
-Hint Immediate In_eq Inf_lt.
+Hint Resolve ListIn_In Sort_NoDup Inf_lt : core.
+Hint Immediate In_eq Inf_lt : core.
 
 End OrderedTypeLists.
 
@@ -66,7 +66,7 @@ Module KeyOrderedType(O:OrderedType).
 
  Definition ltk {elt} : relation (key*elt) := O.lt @@1.
 
- Hint Unfold ltk.
+ Hint Unfold ltk : core.
 
  (* ltk is a strict order *)
 
@@ -109,8 +109,8 @@ Module KeyOrderedType(O:OrderedType).
   Lemma Inf_lt l x x' : ltk x x' -> Inf x' l -> Inf x l.
   Proof. apply InfA_ltA; auto with *. Qed.
 
-  Hint Immediate Inf_eq.
-  Hint Resolve Inf_lt.
+  Hint Immediate Inf_eq : core.
+  Hint Resolve Inf_lt : core.
 
   Lemma Sort_Inf_In l p q : Sort l -> Inf q l -> InA eqk p l -> ltk q p.
   Proof. apply SortA_InfA_InA; auto with *. Qed.
@@ -148,10 +148,10 @@ Module KeyOrderedType(O:OrderedType).
 
  End Elt.
 
- Hint Resolve ltk_not_eqk ltk_not_eqke.
- Hint Immediate Inf_eq.
- Hint Resolve Inf_lt.
- Hint Resolve Sort_Inf_NotIn.
+ Hint Resolve ltk_not_eqk ltk_not_eqke : core.
+ Hint Immediate Inf_eq : core.
+ Hint Resolve Inf_lt : core.
+ Hint Resolve Sort_Inf_NotIn : core.
 
 End KeyOrderedType.