Change Implicit Arguments to Arguments in character

5 files changed, 59 insertions, 59 deletions

diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index 6408b0b..ad0fa32 100644
--- a/mathcomp/character/character.v
+++ b/mathcomp/character/character.v
@@ -390,7 +390,7 @@ Qed.
 
 End StandardRepresentation.
 
-Implicit Arguments grepr0 [R gT G].
+Arguments grepr0 [R gT G].
 Prenex Implicits grepr0 dadd_grepr.
 
 Section Char.
@@ -818,7 +818,7 @@ End IrrClass.
 
 Arguments Scope cfReg [_ group_scope].
 Prenex Implicits cfIirr.
-Implicit Arguments irr_inj [[gT] [G] x1 x2].
+Arguments irr_inj {gT G} [x1 x2].
 
 Section IsChar.
 
@@ -924,7 +924,7 @@ Canonical char_semiringPred := SemiringPred mul_char.
 
 End IsChar.
 Prenex Implicits character.
-Implicit Arguments char_reprP [gT G phi].
+Arguments char_reprP [gT G phi].
 
 Section AutChar.
 
@@ -1870,7 +1870,7 @@ Proof. by apply/eqP; rewrite isom_Iirr_eq0. Qed.
 
 End Isom.
 
-Implicit Arguments isom_Iirr_inj [aT rT G f R x1 x2].
+Arguments isom_Iirr_inj [aT rT G f R] isoGR [x1 x2].
 
 Section IsomInv.
 
@@ -1938,7 +1938,7 @@ Qed.
 
 End Sdprod.
 
-Implicit Arguments sdprod_Iirr_inj [gT K H G x1 x2].
+Arguments sdprod_Iirr_inj [gT K H G] defG [x1 x2].
 
 Section DProd.
 
@@ -2089,7 +2089,7 @@ Proof. by apply/(canLR dprod_IirrK); rewrite dprod_Iirr0. Qed.
 
 End DProd.
 
-Implicit Arguments dprod_Iirr_inj [gT G K H x1 x2].
+Arguments dprod_Iirr_inj [gT G K H] KxH [x1 x2].
 
 Lemma dprod_IirrC (gT : finGroupType) (G K H : {group gT})
                   (KxH : K \x H = G) (HxK : H \x K = G) i j :
@@ -2257,7 +2257,7 @@ Qed.
 
 End Aut.
 
-Implicit Arguments aut_Iirr_inj [gT G x1 x2].
+Arguments aut_Iirr_inj [gT G] u [x1 x2].
 
 Section Coset.
 
@@ -2554,7 +2554,7 @@ Qed.
 
 End DerivedGroup.
 
-Implicit 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 81c26ab..3afaa82 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.
-Implicit 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 Scope classfun_on [_ group_scope group_scope].
 Notation "''CF' ( G , A )" := (classfun_on G A) : ring_scope.
 
-Implicit 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.
-Implicit Arguments orthoPl [phi S].
+Arguments orthoPl [phi S].
 
 Lemma orthogonal_sym : symmetric (@orthogonal _ G).
 Proof.
@@ -1242,12 +1242,12 @@ Qed.
 
 End DotProduct.
 
-Implicit Arguments orthoP [gT G phi psi].
-Implicit Arguments orthoPl [gT G phi S].
-Implicit Arguments orthoPr [gT G S psi].
-Implicit Arguments orthogonalP [gT G R S].
-Implicit Arguments pairwise_orthogonalP [gT G S].
-Implicit 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.
 
-Implicit Arguments dvdn_cforderP [gT G phi n].
+Arguments dvdn_cforderP [gT G phi n].
 
 Section MorphOrder.
 
@@ -1621,7 +1621,7 @@ Proof. exact: cforder_inj_rmorph cfIsom_inj. Qed.
 
 End InvMorphism.
 
-Implicit Arguments cfIsom_inj [aT rT G R f x1 x2].
+Arguments cfIsom_inj [aT rT G f R] isoGR [x1 x2].
 
 Section Coset.
 
@@ -2487,9 +2487,9 @@ Proof. by rewrite rmorphM /= cfAutDprodl cfAutDprodr. Qed.
 
 End FieldAutomorphism.
 
-Implicit Arguments cfAutK [[gT] [G]].
-Implicit Arguments cfAutVK [[gT] [G]].
-Implicit Arguments cfAut_inj [gT G x1 x2].
+Arguments cfAutK u {gT G}.
+Arguments cfAutVK u {gT G}.
+Arguments cfAut_inj u [gT G x1 x2].
 
 Definition conj_cfRes := cfAutRes conjC.
 Definition cfker_conjC := cfker_aut conjC.
diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v
index 9ae289d..7d4a84c 100644
--- a/mathcomp/character/inertia.v
+++ b/mathcomp/character/inertia.v
@@ -569,7 +569,7 @@ End Inertia.
 
 Arguments Scope inertia [_ group_scope cfun_scope].
 Arguments Scope cfclass [_ group_scope cfun_scope group_scope].
-Implicit Arguments conjg_Iirr_inj [gT H x1 x2].
+Arguments conjg_Iirr_inj [gT H] y [x1 x2].
 
 Notation "''I[' phi ] " := (inertia phi) : group_scope.
 Notation "''I[' phi ] " := (inertia_group phi) : Group_scope.
diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v
index 0c1d4c1..fbd4bc3 100644
--- a/mathcomp/character/mxrepresentation.v
+++ b/mathcomp/character/mxrepresentation.v
@@ -427,7 +427,7 @@ Qed.
 
 End OneRepresentation.
 
-Implicit Arguments rkerP [gT G n rG x].
+Arguments rkerP [gT G n rG x].
 
 Section Proper.
 
@@ -819,8 +819,8 @@ Arguments Scope mx_repr [_ _ group_scope nat_scope _].
 Arguments Scope group_ring [_ _ group_scope].
 Arguments Scope regular_repr [_ _ group_scope].
 
-Implicit Arguments centgmxP [R gT G n rG f].
-Implicit 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.
-Implicit 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.
-Implicit 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.
-Implicit 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.
-Implicit 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,19 +2366,19 @@ Qed.
 
 End OneRepresentation.
 
-Implicit Arguments mxmoduleP [gT G n rG m U].
-Implicit Arguments envelop_mxP [gT G n rG A].
-Implicit Arguments hom_mxP [gT G n rG m f W].
-Implicit Arguments rfix_mxP [gT G n rG m W].
-Implicit Arguments cyclic_mxP [gT G n rG u v].
-Implicit Arguments annihilator_mxP [gT G n rG u A].
-Implicit Arguments row_hom_mxP [gT G n rG u v].
-Implicit Arguments mxsimple_isoP [gT G n rG U V].
-Implicit Arguments socleP [gT G n rG sG0 W W'].
-Implicit 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].
 
-Implicit Arguments val_submod_inj [n U m].
-Implicit Arguments val_factmod_inj [n U m].
+Arguments val_submod_inj [n U m].
+Arguments val_factmod_inj [n U m].
 
 Prenex Implicits val_submod_inj val_factmod_inj.
 
@@ -4659,22 +4659,22 @@ Arguments Scope gset_mx [_ _ group_scope group_scope].
 Arguments Scope classg_base [_ _ group_scope group_scope].
 Arguments Scope irrType [_ _ group_scope group_scope].
 
-Implicit Arguments mxmoduleP [F gT G n rG m U].
-Implicit Arguments envelop_mxP [F gT G n rG A].
-Implicit Arguments hom_mxP [F gT G n rG m f W].
-Implicit Arguments mx_Maschke [F gT G n U].
-Implicit Arguments rfix_mxP [F gT G n rG m W].
-Implicit Arguments cyclic_mxP [F gT G n rG u v].
-Implicit Arguments annihilator_mxP [F gT G n rG u A].
-Implicit Arguments row_hom_mxP [F gT G n rG u v].
-Implicit Arguments mxsimple_isoP [F gT G n rG U V].
-Implicit Arguments socle_exists [F gT G n].
-Implicit Arguments socleP [F gT G n rG sG0 W W'].
-Implicit Arguments mx_abs_irrP [F gT G n rG].
-Implicit Arguments socle_rsimP [F gT G n rG sG W1 W2].
-
-Implicit Arguments val_submod_inj [F n U m].
-Implicit Arguments val_factmod_inj [F n U m].
+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 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 val_submod_inj [F n U m].
+Arguments val_factmod_inj [F n U m].
 Prenex Implicits val_submod_inj val_factmod_inj.
 
 Notation "'Cl" := (Clifford_action _) : action_scope.
diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v
index 97ad828..5c9ca9b 100644
--- a/mathcomp/character/vcharacter.v
+++ b/mathcomp/character/vcharacter.v
@@ -709,7 +709,7 @@ End MoreVchar.
 
 Definition dirr (gT : finGroupType) (B : {set gT}) : pred_class :=  
   [pred f : 'CF(B) | (f \in irr B) || (- f \in irr B)].
-Implicit Arguments dirr [[gT]].
+Arguments dirr {gT}.
 
 Section Norm1vchar.