diff options
| author | Anton Trunov | 2018-11-26 14:48:50 +0100 |
|---|---|---|
| committer | Anton Trunov | 2018-12-11 12:13:06 +0100 |
| commit | 2e6e0001f8215e3c42f2557df42e0d6486035c07 (patch) | |
| tree | 10e3129f0584233d7fb825973794b517371c6024 /mathcomp/fingroup | |
| parent | 316cca94aef28c2023cd823c588b140e13d0aded (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.v | 2 | ||||
| -rw-r--r-- | mathcomp/fingroup/fingroup.v | 18 | ||||
| -rw-r--r-- | mathcomp/fingroup/morphism.v | 2 | ||||
| -rw-r--r-- | mathcomp/fingroup/perm.v | 2 |
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. |
