From 2e6e0001f8215e3c42f2557df42e0d6486035c07 Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Mon, 26 Nov 2018 14:48:50 +0100
Subject: 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]
```
---
 mathcomp/fingroup/automorphism.v |  2 +-
 mathcomp/fingroup/fingroup.v     | 18 +++++++++---------
 mathcomp/fingroup/morphism.v     |  2 +-
 mathcomp/fingroup/perm.v         |  2 +-
 4 files changed, 12 insertions(+), 12 deletions(-)

(limited to 'mathcomp/fingroup')

diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v
index 320331c..5f28b7d 100644
--- a/mathcomp/fingroup/automorphism.v
+++ b/mathcomp/fingroup/automorphism.v
@@ -449,7 +449,7 @@ End Characteristicity.
 
 Arguments characteristic _ _%g _%g.
 Notation "H \char G" := (characteristic H G) : group_scope.
-Hint Resolve char_refl.
+Hint Resolve char_refl : core.
 
 Section InjmChar.
 
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index 19cefcd..f436102 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -492,7 +492,7 @@ Qed.
 
 End PreGroupIdentities.
 
-Hint Resolve commute1.
+Hint Resolve commute1 : core.
 Arguments invg_inj {T} [x1 x2].
 Prenex Implicits commute invgK.
 
@@ -1358,7 +1358,7 @@ Lemma valG : val G = G. Proof. by []. Qed.
 (* Non-triviality. *)
 
 Lemma group1 : 1 \in G. Proof. by case/group_setP: (valP G). Qed.
-Hint Resolve group1.
+Hint Resolve group1 : core.
 
 (* Loads of silly variants to placate the incompleteness of trivial. *)
 (* An alternative would be to upgrade done, pending better support   *)
@@ -1647,7 +1647,7 @@ Proof. by move=> y Gy /=; rewrite -class_rcoset rcoset_id. Qed.
 
 Lemma class_refl x : x \in x ^: G.
 Proof. by apply/imsetP; exists 1; rewrite ?conjg1. Qed.
-Hint Resolve class_refl.
+Hint Resolve class_refl : core.
 
 Lemma class_eqP x y : reflect (x ^: G = y ^: G) (x \in y ^: G).
 Proof.
@@ -1794,7 +1794,7 @@ Proof. by move=> x y Gx Gy; apply: val_inj; rewrite /= !subgK ?groupM. Qed.
 
 End OneGroup.
 
-Hint Resolve group1.
+Hint Resolve group1 : core.
 
 Lemma groupD1_inj G H : G^# = H^# -> G :=: H.
 Proof. by move/(congr1 (setU 1)); rewrite !setD1K. Qed.
@@ -1842,9 +1842,9 @@ Qed.
 
 End GroupProp.
 
-Hint Resolve group1 group1_class1 group1_class12 group1_class12.
-Hint Resolve group1_eqType group1_finType.
-Hint Resolve cardG_gt0 cardG_gt0_reduced indexg_gt0.
+Hint Resolve group1 group1_class1 group1_class12 group1_class12 : core.
+Hint Resolve group1_eqType group1_finType : core.
+Hint Resolve cardG_gt0 cardG_gt0_reduced indexg_gt0 : core.
 
 Notation "G :^ x" := (conjG_group G x) : Group_scope.
 
@@ -1907,7 +1907,7 @@ Proof. exact: cardG_gt0. Qed.
 
 End GroupInter.
 
-Hint Resolve order_gt0.
+Hint Resolve order_gt0 : core.
 
 Arguments generated_group _ _%g.
 Arguments joing_group _ _%g _%g.
@@ -3005,7 +3005,7 @@ Notation "''C_' G [ x ]" := (setI_group G 'C[x]) : Group_scope.
 Notation "''C_' ( G ) [ x ]" := (setI_group G 'C[x])
   (only parsing) : Group_scope.
 
-Hint Resolve normG normal_refl.
+Hint Resolve normG normal_refl : core.
 
 Section MinMaxGroup.
 
diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v
index 4b2d863..cb02991 100644
--- a/mathcomp/fingroup/morphism.v
+++ b/mathcomp/fingroup/morphism.v
@@ -1495,7 +1495,7 @@ Proof. by apply/injmP; apply: in2W; apply: subg_inj. Qed.
 
 Lemma injm_subg : 'injm (subg G).
 Proof. by apply/injmP; apply: can_in_inj (@subgK _ _). Qed.
-Hint Resolve injm_sgval injm_subg.
+Hint Resolve injm_sgval injm_subg : core.
 
 Lemma ker_sgval : 'ker sgval = 1. Proof. exact/trivgP. Qed.
 Lemma ker_subg : 'ker (subg G) = 1. Proof. exact/trivgP. Qed.
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index 01ef08e..b1a7dd7 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -129,7 +129,7 @@ Lemma perm_inj s : injective s.
 Proof. by rewrite -!pvalE; apply: (injectiveP _ (valP s)). Qed.
 
 Arguments perm_inj : clear implicits.
-Hint Resolve perm_inj.
+Hint Resolve perm_inj : core.
 
 Lemma perm_onto s : codom s =i predT.
 Proof. by apply/subset_cardP; rewrite ?card_codom ?subset_predT. Qed.
-- 
cgit v1.2.3