Merge Arguments and Prenex Implicits

See the discussion here:
https://github.com/math-comp/math-comp/pull/242#discussion_r233778114

10 files changed, 49 insertions, 57 deletions

diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v
index 7ca0bdb..5f1a013 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -196,7 +196,7 @@ Arguments Ohm _%N _ _%g.
 Arguments Ohm_group _%N _ _%g.
 Arguments Mho _%N _ _%g.
 Arguments Mho_group _%N _ _%g.
-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.
-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.
-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.
-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.
-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.
 
-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].
+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.
 
@@ -2023,9 +2023,8 @@ Qed.
 
 End AbelianStructure.
 
-Arguments abelian_type _ _%g.
-Arguments homocyclic _ _%g.
-Prenex Implicits abelian_type homocyclic.
+Arguments abelian_type {_} _%g.
+Arguments homocyclic {_} _%g.
 
 Section IsogAbelian.
 
diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v
index f984960..98434ba 100644
--- a/mathcomp/solvable/center.v
+++ b/mathcomp/solvable/center.v
@@ -187,7 +187,7 @@ End Injm.
 
 End Center.
 
-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 ffb07d2..dcd53ce 100644
--- a/mathcomp/solvable/commutator.v
+++ b/mathcomp/solvable/commutator.v
@@ -352,7 +352,7 @@ Proof. exact: commG1P. Qed.
 
 End Commutator_properties.
 
-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 bed8c5c..046f4a2 100644
--- a/mathcomp/solvable/cyclic.v
+++ b/mathcomp/solvable/cyclic.v
@@ -289,11 +289,11 @@ Proof. by rewrite /order => /(<[a]> =P _)->. Qed.
 
 End Cyclic.
 
-Arguments cyclic _ _%g.
-Arguments generator _ _%g _%g.
-Arguments expg_invn _ _%g _%N.
-Arguments cyclicP [gT A].
-Prenex Implicits cyclic Zpm generator expg_invn.
+Arguments cyclic {_} _%g.
+Arguments generator {_}_%g _%g.
+Arguments expg_invn {_} _%g _%N.
+Arguments cyclicP {gT A}.
+Prenex Implicits cyclic Zpm.
 
 (* Euler's theorem *)
 Theorem Euler_exp_totient a n : coprime a n -> a ^ totient n  = 1 %[mod n].
@@ -556,9 +556,8 @@ Qed.
 
 End Metacyclic.
 
-Arguments metacyclic _ _%g.
-Prenex Implicits metacyclic.
-Arguments metacyclicP [gT A].
+Arguments metacyclic {_} _%g.
+Arguments metacyclicP {gT A}.
 
 (* Automorphisms of cyclic groups. *)
 Section CyclicAutomorphism.
diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v
index 98657b4..f7edfc9 100644
--- a/mathcomp/solvable/frobenius.v
+++ b/mathcomp/solvable/frobenius.v
@@ -244,7 +244,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.
-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
@@ -620,9 +620,9 @@ Qed.
 
 End FrobeniusBasics.
 
-Arguments normedTI_P [gT A G L].
-Arguments normedTI_memJ_P [gT A G L].
-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 c5b5c0c..a1830b9 100644
--- a/mathcomp/solvable/gseries.v
+++ b/mathcomp/solvable/gseries.v
@@ -71,17 +71,16 @@ Definition simple A := minnormal A A.
 Definition chief_factor A V U := maxnormal V U A && (U <| A).
 End GroupDefs.
 
-Arguments subnormal _ _%g _%g.
+Arguments subnormal {_} _%g _%g.
 Arguments invariant_factor _ _%g _%g _%g.
 Arguments stable_factor _ _%g _%g _%g.
 Arguments central_factor _ _%g _%g _%g.
-Arguments maximal _ _%g _%g.
+Arguments maximal {_} _%g _%g.
 Arguments maximal_eq _ _%g _%g.
 Arguments maxnormal _ _%g _%g _%g.
 Arguments minnormal _ _%g _%g.
-Arguments simple _ _%g.
+Arguments simple {_} _%g.
 Arguments chief_factor _ _%g _%g _%g.
-Prenex Implicits subnormal maximal simple.
 
 Notation "H <|<| G" := (subnormal H G)
   (at level 70, no associativity) : group_scope.
@@ -212,8 +211,7 @@ Qed.
 
 End Subnormal.
 
-Arguments subnormalP [gT H G].
-Prenex Implicits subnormalP.
+Arguments subnormalP {gT H G}.
 
 Section MorphSubNormal.
 
diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v
index c1a2eb5..5f7a9ed 100644
--- a/mathcomp/solvable/maximal.v
+++ b/mathcomp/solvable/maximal.v
@@ -1649,4 +1649,4 @@ Qed.
 
 End SCN.
 
-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/nilpotent.v b/mathcomp/solvable/nilpotent.v
index 387ce34..d631919 100644
--- a/mathcomp/solvable/nilpotent.v
+++ b/mathcomp/solvable/nilpotent.v
@@ -75,10 +75,9 @@ Definition solvable :=
 
 End PropertiesDefs.
 
-Arguments nilpotent _ _%g.
-Arguments nil_class _ _%g.
-Arguments solvable _ _%g.
-Prenex Implicits nil_class nilpotent solvable.
+Arguments nilpotent {_} _%g.
+Arguments nil_class {_} _%g.
+Arguments solvable {_} _%g.
 
 Section NilpotentProps.
 
diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v
index 6507160..6c02e7b 100644
--- a/mathcomp/solvable/pgroup.v
+++ b/mathcomp/solvable/pgroup.v
@@ -83,16 +83,15 @@ Definition Sylow A B := p_group B && Hall A B.
 
 End PgroupDefs.
 
-Arguments pgroup _ _%N _%g.
+Arguments pgroup {_} _%N _%g.
 Arguments psubgroup _ _%N _%g _%g.
 Arguments p_group _ _%g.
 Arguments p_elt _ _%N.
 Arguments constt _ _%g _%N.
-Arguments Hall _ _%g _%g.
+Arguments Hall {_} _%g _%g.
 Arguments pHall _ _%N _%g _%g.
 Arguments Syl _ _%N _%g.
-Arguments Sylow _ _%g _%g.
-Prenex Implicits p_group Hall Sylow.
+Arguments Sylow {_} _%g _%g.
 
 Notation "pi .-group" := (pgroup pi)
   (at level 2, format "pi .-group") : group_scope.
@@ -170,7 +169,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.
-Arguments pgroupP [pi G].
+Arguments pgroupP {pi G}.
 
 Lemma pgroup1 pi : pi.-group [1 gT].
 Proof. by rewrite /pgroup cards1. Qed.
@@ -679,9 +678,8 @@ Qed.
 
 End PgroupProps.
 
-Arguments pgroupP [gT pi G].
-Arguments constt1P [gT pi x].
-Prenex Implicits pgroupP constt1P.
+Arguments pgroupP {gT pi G}.
+Arguments constt1P {gT pi x}.
 
 Section NormalHall.
 
@@ -1302,8 +1300,8 @@ Qed.
 
 End EqPcore.
 
-Arguments sdprod_Hall_pcoreP [pi gT H G].
-Arguments sdprod_Hall_p'coreP [gT pi H G].
+Arguments sdprod_Hall_pcoreP {pi gT H G}.
+Arguments sdprod_Hall_p'coreP {gT pi H G}.
 
 Section Injm.
 
diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v
index dd45afa..f940ec9 100644
--- a/mathcomp/solvable/sylow.v
+++ b/mathcomp/solvable/sylow.v
@@ -535,8 +535,7 @@ Qed.
 
 End Zgroups.
 
-Arguments Zgroup _ _%g.
-Prenex Implicits Zgroup.
+Arguments Zgroup {_} _%g.
 
 Section NilPGroups.