aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/fingroup
diff options
context:
space:
mode:
authorAnton Trunov2018-11-26 14:48:50 +0100
committerAnton Trunov2018-12-11 12:13:06 +0100
commit2e6e0001f8215e3c42f2557df42e0d6486035c07 (patch)
tree10e3129f0584233d7fb825973794b517371c6024 /mathcomp/fingroup
parent316cca94aef28c2023cd823c588b140e13d0aded (diff)
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] ```
Diffstat (limited to 'mathcomp/fingroup')
-rw-r--r--mathcomp/fingroup/automorphism.v2
-rw-r--r--mathcomp/fingroup/fingroup.v18
-rw-r--r--mathcomp/fingroup/morphism.v2
-rw-r--r--mathcomp/fingroup/perm.v2
4 files changed, 12 insertions, 12 deletions
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.