Fix some new warnings emitted by Coq 8.10:

```
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
```

10 files changed, 25 insertions, 25 deletions

diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 2db8927..f108ff9 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -558,7 +558,7 @@ Qed.
 
 Lemma mem_index_enum T i : i \in index_enum T.
 Proof. by rewrite -[index_enum T]enumT mem_enum. Qed.
-Hint Resolve mem_index_enum.
+Hint Resolve mem_index_enum : core.
 
 Lemma filter_index_enum T P : filter P (index_enum T) = enum P.
 Proof. by []. Qed.
diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index ed1eedf..80c9312 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -327,7 +327,7 @@ Proof. by case/dvdnP=> n' ->; rewrite /dvdn mulnA modnMl. Qed.
 
 Lemma dvdn_mulr d m n : d %| m -> d %| m * n.
 Proof. by move=> d_m; rewrite mulnC dvdn_mull. Qed.
-Hint Resolve dvdn0 dvd1n dvdnn dvdn_mull dvdn_mulr.
+Hint Resolve dvdn0 dvd1n dvdnn dvdn_mull dvdn_mulr : core.
 
 Lemma dvdn_mul d1 d2 m1 m2 : d1 %| m1 -> d2 %| m2 -> d1 * d2 %| m1 * m2.
 Proof.
@@ -462,7 +462,7 @@ case: m => //= m; elim: n => //= n IHn; rewrite ltnS leq_eqVlt.
 by case/predU1P=> [-> | /IHn]; [apply: dvdn_mulr | apply: dvdn_mull].
 Qed.
 
-Hint Resolve dvdn_add dvdn_sub dvdn_exp.
+Hint Resolve dvdn_add dvdn_sub dvdn_exp : core.
 
 Lemma eqn_mod_dvd d m n : n <= m -> (m == n %[mod d]) = (d %| m - n).
 Proof.
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 6ed4b97..dc3daf0 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -196,7 +196,7 @@ Notation eqxx := eq_refl.
 Lemma eq_sym (T : eqType) (x y : T) : (x == y) = (y == x).
 Proof. exact/eqP/eqP. Qed.
 
-Hint Resolve eq_refl eq_sym.
+Hint Resolve eq_refl eq_sym : core.
 
 Section Contrapositives.
 
diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index c534b7b..5358dc7 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -216,7 +216,7 @@ Definition closure_mem m_a : pred T :=
 
 End Connect.
 
-Hint Resolve connect0.
+Hint Resolve connect0 : core.
 
 Notation n_comp e a := (n_comp_mem e (mem a)).
 Notation closed e a := (closed_mem e (mem a)).
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 4ad02c6..9ca96c8 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -244,7 +244,7 @@ End BasicSetTheory.
 Definition inE := (in_set, inE).
 
 Arguments set0 {T}.
-Hint Resolve in_setT.
+Hint Resolve in_setT : core.
 
 Notation "[ 'set' : T ]" := (setTfor (Phant T))
   (at level 0, format "[ 'set' :  T ]") : set_scope.
@@ -348,7 +348,7 @@ Proof. by apply/subsetP=> x; rewrite inE. Qed.
 
 Lemma subsetT_hint mA : subset mA (mem [set: T]).
 Proof. by rewrite unlock; apply/pred0P=> x; rewrite !inE. Qed.
-Hint Resolve subsetT_hint.
+Hint Resolve subsetT_hint : core.
 
 Lemma subTset A : (setT \subset A) = (A == setT).
 Proof. by rewrite eqEsubset subsetT. Qed.
@@ -975,7 +975,7 @@ Arguments subUsetP {T A B C}.
 Arguments subsetDP {T A B C}.
 Arguments subsetD1P {T A B x}.
 Prenex Implicits set1.
-Hint Resolve subsetT_hint.
+Hint Resolve subsetT_hint : core.
 
 Section setOpsAlgebra.
 
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 8be2eb0..441fc12 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -626,7 +626,7 @@ Lemma subxx_hint (mA : mem_pred T) : subset mA mA.
 Proof.
 by case: mA => A; have:= introT (subsetP A A); rewrite !unlock => ->.
 Qed.
-Hint Resolve subxx_hint.
+Hint Resolve subxx_hint : core.
 
 (* The parametrization by predType makes it easier to apply subxx. *)
 Lemma subxx (pT : predType T) (pA : pT) : pA \subset pA.
@@ -818,7 +818,7 @@ Proof. by rewrite !disjoint_has has_cat negb_or. Qed.
 
 End OpsTheory.
 
-Hint Resolve subxx_hint.
+Hint Resolve subxx_hint : core.
 
 Arguments pred0P {T P}.
 Arguments pred0Pn {T P}.
@@ -1585,7 +1585,7 @@ End OrdinalSub.
 Notation "''I_' n" := (ordinal n)
   (at level 8, n at level 2, format "''I_' n").
 
-Hint Resolve ltn_ord.
+Hint Resolve ltn_ord : core.
 
 Section OrdinalEnum.
 
diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v
index f30c3a1..b7a8444 100644
--- a/mathcomp/ssreflect/generic_quotient.v
+++ b/mathcomp/ssreflect/generic_quotient.v
@@ -491,7 +491,7 @@ Proof. by apply: right_trans; [apply: equiv_sym|apply: equiv_trans]. Qed.
 
 End EquivRel.
 
-Hint Resolve equiv_refl.
+Hint Resolve equiv_refl : core.
 
 Notation EquivRel r er es et := (@EquivRelPack _ r (EquivClass er es et)).
 Notation "[ 'equiv_rel' 'of' e ]" := (@equiv_pack _ _ e _ id)
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 02064c3..2a07d17 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -358,7 +358,7 @@ Proof. by case/primeP. Qed.
 Lemma prime_gt0 p : prime p -> 0 < p.
 Proof. by move/prime_gt1; apply: ltnW. Qed.
 
-Hint Resolve prime_gt1 prime_gt0.
+Hint Resolve prime_gt1 prime_gt0 : core.
 
 Lemma prod_prime_decomp n :
   n > 0 -> n = \prod_(f <- prime_decomp n) f.1 ^ f.2.
@@ -494,7 +494,7 @@ Proof. by case: n => [|[|n]] //; rewrite prime_gt0 ?pdiv_prime. Qed.
 
 Lemma max_pdiv_gt0 n : 0 < max_pdiv n.
 Proof. by case: n => [|[|n]] //; rewrite prime_gt0 ?max_pdiv_prime. Qed.
-Hint Resolve pdiv_gt0 max_pdiv_gt0.
+Hint Resolve pdiv_gt0 max_pdiv_gt0 : core.
 
 Lemma pdiv_min_dvd m d : 1 < d -> d %| m -> pdiv m <= d.
 Proof.
@@ -636,7 +636,7 @@ Proof. by rewrite lognE dvdn1 /= andbC; case: eqP => // ->. Qed.
 
 Lemma pfactor_gt0 p n : 0 < p ^ logn p n.
 Proof. by rewrite expn_gt0 lognE; case: (posnP p) => // ->. Qed.
-Hint Resolve pfactor_gt0.
+Hint Resolve pfactor_gt0 : core.
 
 Lemma pfactor_dvdn p n m : prime p -> m > 0 -> (p ^ n %| m) = (n <= logn p m).
 Proof.
@@ -858,7 +858,7 @@ Qed.
 
 Lemma part_gt0 pi n : 0 < n`_pi.
 Proof. exact: prodn_gt0. Qed.
-Hint Resolve part_gt0.
+Hint Resolve part_gt0 : core.
 
 Lemma sub_in_partn pi1 pi2 n :
   {in \pi(n), {subset pi1 <= pi2}} -> n`_pi1 %| n`_pi2.
@@ -1219,7 +1219,7 @@ Lemma odd_2'nat n : odd n = 2^'.-nat n.
 Proof. by case: n => // n; rewrite p'natE // dvdn2 negbK. Qed.
 
 End PnatTheory.
-Hint Resolve part_gt0.
+Hint Resolve part_gt0 : core.
 
 (************************************)
 (* Properties of the divisors list. *)
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index ba1f969..2c9fd64 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -1422,7 +1422,7 @@ Qed.
 
 Lemma perm_eq_refl s : perm_eq s s.
 Proof. exact/perm_eqP. Qed.
-Hint Resolve perm_eq_refl.
+Hint Resolve perm_eq_refl : core.
 
 Lemma perm_eq_sym : symmetric perm_eq.
 Proof. by move=> s1 s2; apply/perm_eqP/perm_eqP=> ? ?. Qed.
@@ -1601,7 +1601,7 @@ Arguments perm_eqP {T s1 s2}.
 Arguments perm_eqlP {T s1 s2}.
 Arguments perm_eqrP {T s1 s2}.
 Prenex Implicits perm_eq.
-Hint Resolve perm_eq_refl.
+Hint Resolve perm_eq_refl : core.
 
 Section RotrLemmas.
 
@@ -1827,7 +1827,7 @@ Qed.
 
 Lemma subseq_refl s : subseq s s.
 Proof. by elim: s => //= x s IHs; rewrite eqxx. Qed.
-Hint Resolve subseq_refl.
+Hint Resolve subseq_refl : core.
 
 Lemma cat_subseq s1 s2 s3 s4 :
   subseq s1 s3 -> subseq s2 s4 -> subseq (s1 ++ s2) (s3 ++ s4).
@@ -1876,7 +1876,7 @@ End Subseq.
 Prenex Implicits subseq.
 Arguments subseqP {T s1 s2}.
 
-Hint Resolve subseq_refl.
+Hint Resolve subseq_refl : core.
 
 Section Rem.
 
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index b8388f0..581a7ee 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -316,11 +316,11 @@ Lemma leq0n n : 0 <= n.                 Proof. by []. Qed.
 Lemma ltn0Sn n : 0 < n.+1.              Proof. by []. Qed.
 Lemma ltn0 n : n < 0 = false.           Proof. by []. Qed.
 Lemma leqnn n : n <= n.                 Proof. by elim: n. Qed.
-Hint Resolve leqnn.
+Hint Resolve leqnn : core.
 Lemma ltnSn n : n < n.+1.               Proof. by []. Qed.
 Lemma eq_leq m n : m = n -> m <= n.     Proof. by move->. Qed.
 Lemma leqnSn n : n <= n.+1.             Proof. by elim: n. Qed.
-Hint Resolve leqnSn.
+Hint Resolve leqnSn : core.
 Lemma leq_pred n : n.-1 <= n.           Proof. by case: n => /=. Qed.
 Lemma leqSpred n : n <= n.-1.+1.        Proof. by case: n => /=. Qed.
 
@@ -344,7 +344,7 @@ Lemma lt0n n : (0 < n) = (n != 0).             Proof. by case: n. Qed.
 Lemma lt0n_neq0 n : 0 < n -> n != 0.           Proof. by case: n. Qed.
 Lemma eqn0Ngt n : (n == 0) = ~~ (n > 0).       Proof. by case: n. Qed.
 Lemma neq0_lt0n n : (n == 0) = false -> 0 < n. Proof. by case: n. Qed.
-Hint Resolve lt0n_neq0 neq0_lt0n.
+Hint Resolve lt0n_neq0 neq0_lt0n : core.
 
 Lemma eqn_leq m n : (m == n) = (m <= n <= m).
 Proof. by elim: m n => [|m IHm] []. Qed.
@@ -375,7 +375,7 @@ Proof. by move=> Hmn; apply: leq_trans. Qed.
 
 Lemma ltnW m n : m < n -> m <= n.
 Proof. exact: leq_trans. Qed.
-Hint Resolve ltnW.
+Hint Resolve ltnW : core.
 
 Lemma leqW m n : m <= n -> m <= n.+1.
 Proof. by move=> le_mn; apply: ltnW. Qed.