Merge pull request #179 from jashug/deprecate-implicit-arguments

Remove Implicit Arguments command in favor of Arguments

10 files changed, 34 insertions, 34 deletions

diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v
index 2b0ab00..f3ff7c3 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -196,7 +196,7 @@ Arguments Scope Ohm [nat_scope _ group_scope].
 Arguments Scope Ohm_group [nat_scope _ group_scope].
 Arguments Scope Mho [nat_scope _ group_scope].
 Arguments Scope Mho_group [nat_scope _ group_scope].
-Implicit Arguments OhmPredP [n gT x].
+Arguments OhmPredP [n gT x].
 
 Notation "''Ohm_' n ( G )" := (Ohm n G)
   (at level 8, n at level 2, format "''Ohm_' n ( G )") : group_scope.
@@ -233,7 +233,7 @@ apply: (iffP (dvdn_biglcmP _ _ _)) => eAn x Ax.
   by apply/eqP; rewrite -order_dvdn eAn.
 by rewrite order_dvdn eAn.
 Qed.
-Implicit Arguments exponentP [A n].
+Arguments exponentP [A n].
 
 Lemma trivg_exponent G : (G :==: 1) = (exponent G %| 1).
 Proof.
@@ -495,7 +495,7 @@ Qed.
 
 Lemma pElemP p A E : reflect (E \subset A /\ p.-abelem E) (E \in 'E_p(A)).
 Proof. by rewrite inE; apply: andP. Qed.
-Implicit Arguments pElemP [p A E].
+Arguments pElemP [p A E].
 
 Lemma pElemS p A B : A \subset B -> 'E_p(A) \subset 'E_p(B).
 Proof.
@@ -511,7 +511,7 @@ Proof. by rewrite !inE conjSg abelemJ. Qed.
 Lemma pnElemP p n A E :
   reflect [/\ E \subset A, p.-abelem E & logn p #|E| = n] (E \in 'E_p^n(A)).
 Proof. by rewrite !inE -andbA; apply: (iffP and3P) => [] [-> -> /eqP]. Qed.
-Implicit Arguments pnElemP [p n A E].
+Arguments pnElemP [p n A E].
 
 Lemma pnElemPcard p n A E :
   E \in 'E_p^n(A) -> [/\ E \subset A, p.-abelem E & #|E| = p ^ n]%N.
@@ -636,7 +636,7 @@ have:= EpnE; rewrite pnElemE ?(pnElem_prime EpnE) // !inE -andbA ltnS.
 case/and3P=> sEG _ oE; rewrite dvdn_leq // (dvdn_trans _ (cardSg sEG)) //.
 by rewrite (eqP oE) dvdn_exp.
 Qed.
-Implicit Arguments nElemP [n G E].
+Arguments nElemP [n G E].
 
 Lemma nElem0 G : 'E^0(G) = [set 1%G].
 Proof.
@@ -899,18 +899,18 @@ Qed.
 
 End ExponentAbelem.
 
-Implicit Arguments LdivP [gT A n x].
-Implicit Arguments exponentP [gT A n].
-Implicit Arguments abelemP [gT p G].
-Implicit Arguments is_abelemP [gT G].
-Implicit Arguments pElemP [gT p A E].
-Implicit Arguments pnElemP [gT p n A E].
-Implicit Arguments nElemP [gT n G E].
-Implicit Arguments nElem1P [gT G E].
-Implicit Arguments pmaxElemP [gT p A E].
-Implicit Arguments pmaxElem_LdivP [gT p G E].
-Implicit Arguments p_rank_geP [gT p n G].
-Implicit Arguments rank_geP [gT n G].
+Arguments LdivP [gT A n x].
+Arguments exponentP [gT A n].
+Arguments abelemP [gT p G].
+Arguments is_abelemP [gT G].
+Arguments pElemP [gT p A E].
+Arguments pnElemP [gT p n A E].
+Arguments nElemP [gT n G E].
+Arguments nElem1P [gT G E].
+Arguments pmaxElemP [gT p A E].
+Arguments pmaxElem_LdivP [gT p G E].
+Arguments p_rank_geP [gT p n G].
+Arguments rank_geP [gT n G].
 
 Section MorphAbelem.
 
diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v
index d9010d5..1c804cc 100644
--- a/mathcomp/solvable/burnside_app.v
+++ b/mathcomp/solvable/burnside_app.v
@@ -26,7 +26,7 @@ rewrite big_uniq // -(card_uniqP Us) (eq_card sG) -Frobenius_Cauchy.
 by apply/actsP=> ? _ ?; rewrite !inE.
 Qed.
 
-Implicit Arguments burnside_formula [gT].
+Arguments burnside_formula [gT].
 
 Section colouring.
 
diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v
index 54726be..c461a9e 100644
--- a/mathcomp/solvable/center.v
+++ b/mathcomp/solvable/center.v
@@ -187,7 +187,7 @@ End Injm.
 
 End Center.
 
-Implicit Arguments center_idP [gT A].
+Arguments center_idP [gT A].
 
 Lemma isog_center (aT rT : finGroupType) (G : {group aT}) (H : {group rT}) :
   G \isog H -> 'Z(G) \isog 'Z(H).
diff --git a/mathcomp/solvable/commutator.v b/mathcomp/solvable/commutator.v
index 1f9bad0..6a390ce 100644
--- a/mathcomp/solvable/commutator.v
+++ b/mathcomp/solvable/commutator.v
@@ -352,7 +352,7 @@ Proof. exact: commG1P. Qed.
 
 End Commutator_properties.
 
-Implicit Arguments derG1P [gT G].
+Arguments derG1P [gT G].
 
 Lemma der_cont n : GFunctor.continuous (derived_at n).
 Proof. by move=> aT rT G f; rewrite morphim_der. Qed.
diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v
index 9a1e451..7663163 100644
--- a/mathcomp/solvable/cyclic.v
+++ b/mathcomp/solvable/cyclic.v
@@ -292,7 +292,7 @@ End Cyclic.
 Arguments Scope cyclic [_ group_scope].
 Arguments Scope generator [_ group_scope group_scope].
 Arguments Scope expg_invn [_ group_scope nat_scope].
-Implicit Arguments cyclicP [gT A].
+Arguments cyclicP [gT A].
 Prenex Implicits cyclic Zpm generator expg_invn.
 
 (* Euler's theorem *)
@@ -558,7 +558,7 @@ End Metacyclic.
 
 Arguments Scope metacyclic [_ group_scope].
 Prenex Implicits metacyclic.
-Implicit Arguments metacyclicP [gT A].
+Arguments metacyclicP [gT A].
 
 (* Automorphisms of cyclic groups. *)
 Section CyclicAutomorphism.
diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v
index da65950..3416587 100644
--- a/mathcomp/solvable/frobenius.v
+++ b/mathcomp/solvable/frobenius.v
@@ -246,7 +246,7 @@ have Gg: g \in G by rewrite groupMl ?groupV.
 rewrite -conjIg (inj_eq (act_inj 'Js x)) (eq_sym A) (sameP eqP normP).
 by rewrite -cards_eq0 cardJg cards_eq0 setI_eq0 => /tiAG/(subsetP nAL)->.
 Qed.
-Implicit Arguments normedTI_P [A G L].
+Arguments normedTI_P [A G L].
 
 Lemma normedTI_memJ_P A G L :
   reflect [/\ A != set0, L \subset G
@@ -622,9 +622,9 @@ Qed.
 
 End FrobeniusBasics.
 
-Implicit Arguments normedTI_P [gT A G L].
-Implicit Arguments normedTI_memJ_P [gT A G L].
-Implicit Arguments Frobenius_kerP [gT G K].
+Arguments normedTI_P [gT A G L].
+Arguments normedTI_memJ_P [gT A G L].
+Arguments Frobenius_kerP [gT G K].
 
 Lemma Frobenius_coprime_quotient (gT : finGroupType) (G K H N : {group gT}) :
     K ><| H = G -> N <| G -> coprime #|K| #|H| /\ H :!=: 1%g ->
diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v
index 6dcd833..1dc6a35 100644
--- a/mathcomp/solvable/gseries.v
+++ b/mathcomp/solvable/gseries.v
@@ -212,7 +212,7 @@ Qed.
 
 End Subnormal.
 
-Implicit Arguments subnormalP [gT G H].
+Arguments subnormalP [gT H G].
 Prenex Implicits subnormalP.
 
 Section MorphSubNormal.
diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v
index e5c2d4f..06cf329 100644
--- a/mathcomp/solvable/maximal.v
+++ b/mathcomp/solvable/maximal.v
@@ -1649,4 +1649,4 @@ Qed.
 
 End SCN.
 
-Implicit Arguments SCN_P [gT G A].
\ No newline at end of file
+Arguments SCN_P [gT G A].
\ No newline at end of file
diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v
index b595530..d383aa7 100644
--- a/mathcomp/solvable/pgroup.v
+++ b/mathcomp/solvable/pgroup.v
@@ -170,7 +170,7 @@ Proof. exact: partn_eq1 (cardG_gt0 G). Qed.
 Lemma pgroupP pi G :
   reflect (forall p, prime p -> p %| #|G| -> p \in pi) (pi.-group G).
 Proof. exact: pnatP. Qed.
-Implicit Arguments pgroupP [pi G].
+Arguments pgroupP [pi G].
 
 Lemma pgroup1 pi : pi.-group [1 gT].
 Proof. by rewrite /pgroup cards1. Qed.
@@ -679,8 +679,8 @@ Qed.
 
 End PgroupProps.
 
-Implicit Arguments pgroupP [gT pi G].
-Implicit Arguments constt1P [gT pi x].
+Arguments pgroupP [gT pi G].
+Arguments constt1P [gT pi x].
 Prenex Implicits pgroupP constt1P.
 
 Section NormalHall.
@@ -1302,8 +1302,8 @@ Qed.
 
 End EqPcore.
 
-Implicit Arguments sdprod_Hall_pcoreP [gT pi G H].
-Implicit Arguments sdprod_Hall_p'coreP [gT pi G H].
+Arguments sdprod_Hall_pcoreP [pi gT H G].
+Arguments sdprod_Hall_p'coreP [gT pi H G].
 
 Section Injm.
 
diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v
index ae60ce0..c0ab34b 100644
--- a/mathcomp/solvable/primitive_action.v
+++ b/mathcomp/solvable/primitive_action.v
@@ -187,7 +187,7 @@ End NTransitive.
 Arguments Scope dtuple_on [_ nat_scope group_scope].
 Arguments Scope ntransitive
   [_ _ nat_scope group_scope group_scope action_scope].
-Implicit Arguments n_act [gT sT n].
+Arguments n_act [gT sT] _ [n].
 
 Notation "n .-dtuple ( S )" := (dtuple_on n S)
   (at level 8, format "n .-dtuple ( S )") : set_scope.