Merge Arguments and Prenex Implicits

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

3 files changed, 46 insertions, 49 deletions

diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index e522924..6752623 100644
--- a/mathcomp/character/character.v
+++ b/mathcomp/character/character.v
@@ -390,8 +390,8 @@ Qed.
 
 End StandardRepresentation.
 
-Arguments grepr0 [R gT G].
-Prenex Implicits grepr0 dadd_grepr.
+Arguments grepr0 {R gT G}.
+Prenex Implicits dadd_grepr.
 
 Section Char.
 
@@ -924,7 +924,7 @@ Canonical char_semiringPred := SemiringPred mul_char.
 
 End IsChar.
 Prenex Implicits character.
-Arguments char_reprP [gT G phi].
+Arguments char_reprP {gT G phi}.
 
 Section AutChar.
 
@@ -2554,7 +2554,7 @@ Qed.
 
 End DerivedGroup.
 
-Arguments irr_prime_injP [gT G i].
+Arguments irr_prime_injP {gT G i}.
 
 (* Determinant characters and determinential order. *)
 Section DetOrder.
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 7a0e538..ac3e5bc 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -557,7 +557,7 @@ rewrite big1 ?addr0 // => _ /andP[/imsetP[y Gy ->]]; apply: contraNeq.
 rewrite cfunE cfun_repr cfun_classE Gy mulf_eq0 => /norP[_].
 by rewrite pnatr_eq0 -lt0n lt0b => /class_eqP->.
 Qed.
-Arguments cfun_onP [A phi].
+Arguments cfun_onP {A phi}.
 
 Lemma cfun_on0 A phi x : phi \in 'CF(G, A) -> x \notin A -> phi x = 0.
 Proof. by move/cfun_onP; apply. Qed.
@@ -759,7 +759,7 @@ End ClassFun.
 Arguments classfun_on _ _%g _%g.
 Notation "''CF' ( G , A )" := (classfun_on G A) : ring_scope.
 
-Arguments cfun_onP [gT G A phi].
+Arguments cfun_onP {gT G A phi}.
 Hint Resolve cfun_onT.
 
 Section DotProduct.
@@ -1009,7 +1009,7 @@ Lemma orthoPl phi S :
 Proof.
 by rewrite [orthogonal _ S]andbT /=; apply: (iffP allP) => ophiS ? /ophiS/eqP.
 Qed.
-Arguments orthoPl [phi S].
+Arguments orthoPl {phi S}.
 
 Lemma orthogonal_sym : symmetric (@orthogonal _ G).
 Proof.
@@ -1242,12 +1242,12 @@ Qed.
 
 End DotProduct.
 
-Arguments orthoP [gT G phi psi].
-Arguments orthoPl [gT G phi S].
-Arguments orthoPr [gT G S psi].
-Arguments orthogonalP [gT G S R].
-Arguments pairwise_orthogonalP [gT G S].
-Arguments orthonormalP [gT G S].
+Arguments orthoP {gT G phi psi}.
+Arguments orthoPl {gT G phi S}.
+Arguments orthoPr {gT G S psi}.
+Arguments orthogonalP {gT G S R}.
+Arguments pairwise_orthogonalP {gT G S}.
+Arguments orthonormalP {gT G S}.
 
 Section CfunOrder.
 
@@ -1273,7 +1273,7 @@ Proof. by apply/eqP; rewrite -dvdn_cforder. Qed.
 
 End CfunOrder.
 
-Arguments dvdn_cforderP [gT G phi n].
+Arguments dvdn_cforderP {gT G phi n}.
 
 Section MorphOrder.
 
diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v
index c8d7ab1..6859168 100644
--- a/mathcomp/character/mxrepresentation.v
+++ b/mathcomp/character/mxrepresentation.v
@@ -427,7 +427,7 @@ Qed.
 
 End OneRepresentation.
 
-Arguments rkerP [gT G n rG x].
+Arguments rkerP {gT G n rG x}.
 
 Section Proper.
 
@@ -819,8 +819,8 @@ Arguments mx_repr _ _ _%g _%N _.
 Arguments group_ring _ _ _%g.
 Arguments regular_repr _ _ _%g.
 
-Arguments centgmxP [R gT G n rG f].
-Arguments rkerP [R gT G n rG x].
+Arguments centgmxP {R gT G n rG f}.
+Arguments rkerP {R gT G n rG x}.
 Prenex Implicits gring_mxK.
 
 Section ChangeOfRing.
@@ -933,7 +933,7 @@ by apply: (iffP subsetP) => modU x Gx; have:= modU x Gx; rewrite !inE ?Gx.
 Qed.
 
 End Stabilisers.
-Arguments mxmoduleP [m U].
+Arguments mxmoduleP {m U}.
 
 Lemma rstabS m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)) :
   (U <= V)%MS -> rstab rG V \subset rstab rG U.
@@ -1288,7 +1288,7 @@ apply/sub_kermxP; rewrite mul_rV_lin1 /=; apply: (canLR vec_mxK).
 apply/row_matrixP=> j; rewrite !row_mul rowK mul_vec_lin /= mul_vec_lin_row.
 by rewrite -!row_mul mulmxBr !mulmxA cGf ?enum_valP // subrr !linear0.
 Qed.
-Arguments hom_mxP [m f W].
+Arguments hom_mxP {m f W}.
 
 Lemma hom_envelop_mxC m f (W : 'M_(m, n)) A :
   (W <= dom_hom_mx f -> A \in E_G -> W *m A *m f = W *m f *m A)%MS.
@@ -1366,7 +1366,7 @@ apply/sub_kermxP; rewrite mul_rV_lin1 /=; apply: (canLR vec_mxK).
 apply/row_matrixP=> i; rewrite row_mul rowK mul_vec_lin_row -row_mul.
 by rewrite mulmxBr mulmx1 cHW ?enum_valP // subrr !linear0.
 Qed.
-Arguments rfix_mxP [m W].
+Arguments rfix_mxP {m W}.
 
 Lemma rfix_mx_id (H : {set gT}) x : x \in H -> rfix_mx H *m rG x = rfix_mx H.
 Proof. exact/rfix_mxP. Qed.
@@ -1428,7 +1428,7 @@ rewrite genmxE; apply: (iffP submxP) => [[a] | [A /submxP[a defA]]] -> {v}.
   by rewrite vec_mxK submxMl.
 by exists a; rewrite mulmxA mul_rV_lin1 /= -defA mxvecK.
 Qed.
-Arguments cyclic_mxP [u v].
+Arguments cyclic_mxP {u v}.
 
 Lemma cyclic_mx_id u : (u <= cyclic_mx u)%MS.
 Proof. by apply/cyclic_mxP; exists 1%:M; rewrite ?mulmx1 ?envelop_mx1. Qed.
@@ -2366,21 +2366,19 @@ Qed.
 
 End OneRepresentation.
 
-Arguments mxmoduleP [gT G n rG m U].
-Arguments envelop_mxP [gT G n rG A].
-Arguments hom_mxP [gT G n rG m f W].
-Arguments rfix_mxP [gT G n rG m W].
-Arguments cyclic_mxP [gT G n rG u v].
-Arguments annihilator_mxP [gT G n rG u A].
-Arguments row_hom_mxP [gT G n rG u v].
-Arguments mxsimple_isoP [gT G n rG U V].
-Arguments socleP [gT G n rG sG0 W W'].
-Arguments mx_abs_irrP [gT G n rG].
+Arguments mxmoduleP {gT G n rG m U}.
+Arguments envelop_mxP {gT G n rG A}.
+Arguments hom_mxP {gT G n rG m f W}.
+Arguments rfix_mxP {gT G n rG m W}.
+Arguments cyclic_mxP {gT G n rG u v}.
+Arguments annihilator_mxP {gT G n rG u A}.
+Arguments row_hom_mxP {gT G n rG u v}.
+Arguments mxsimple_isoP {gT G n rG U V}.
+Arguments socleP {gT G n rG sG0 W W'}.
+Arguments mx_abs_irrP {gT G n rG}.
 
-Arguments val_submod_inj [n U m].
-Arguments val_factmod_inj [n U m].
-
-Prenex Implicits val_submod_inj val_factmod_inj.
+Arguments val_submod_inj {n U m}.
+Arguments val_factmod_inj {n U m}.
 
 Section Proper.
 
@@ -4659,23 +4657,22 @@ Arguments gset_mx _ _ _%g _%g.
 Arguments classg_base _ _ _%g _%g : extra scopes.
 Arguments irrType _ _ _%g _%g : extra scopes.
 
-Arguments mxmoduleP [F gT G n rG m U].
-Arguments envelop_mxP [F gT G n rG A].
-Arguments hom_mxP [F gT G n rG m f W].
+Arguments mxmoduleP {F gT G n rG m U}.
+Arguments envelop_mxP {F gT G n rG A}.
+Arguments hom_mxP {F gT G n rG m f W}.
 Arguments mx_Maschke [F gT G n] rG _ [U].
-Arguments rfix_mxP [F gT G n rG m W].
-Arguments cyclic_mxP [F gT G n rG u v].
-Arguments annihilator_mxP [F gT G n rG u A].
-Arguments row_hom_mxP [F gT G n rG u v].
-Arguments mxsimple_isoP [F gT G n rG U V].
+Arguments rfix_mxP {F gT G n rG m W}.
+Arguments cyclic_mxP {F gT G n rG u v}.
+Arguments annihilator_mxP {F gT G n rG u A}.
+Arguments row_hom_mxP {F gT G n rG u v}.
+Arguments mxsimple_isoP {F gT G n rG U V}.
 Arguments socle_exists [F gT G n].
-Arguments socleP [F gT G n rG sG0 W W'].
-Arguments mx_abs_irrP [F gT G n rG].
-Arguments socle_rsimP [F gT G n rG sG W1 W2].
+Arguments socleP {F gT G n rG sG0 W W'}.
+Arguments mx_abs_irrP {F gT G n rG}.
+Arguments socle_rsimP {F gT G n rG sG W1 W2}.
 
-Arguments val_submod_inj [F n U m].
-Arguments val_factmod_inj [F n U m].
-Prenex Implicits val_submod_inj val_factmod_inj.
+Arguments val_submod_inj {F n U m}.
+Arguments val_factmod_inj {F n U m}.
 
 Notation "'Cl" := (Clifford_action _) : action_scope.