Document parameter names whenever possible

As suggested by @ggonthier
[here](https://github.com/math-comp/math-comp/pull/249#pullrequestreview-177938295)

> One of the design ideas for the `Arguments` command was that it would allow
to centralise the documentation of the application of constants.
In that spirit it would be in my opinion better to make as much use of this
as possible, and to document the parameter names whenever possible,
especially that of implicit parameters.

and
[here](https://github.com/math-comp/math-comp/pull/253#discussion_r237434163):

> As a general rule, defined functional constants should have maximal prenex
implicit arguments, as this facilitates their use as arguments to functionals,
because this mimics the way function constants are treated in functional
programming languages with Hindley-Milner type inference. Conversely, lemmas and
theorems should have on-demand implicit arguments, possibly interspersed with
explicit ones, as it's fairly common for other lemmas to have universally
quantified premises; also, this makes it easier to specify such arguments with
the apply: tactic. This policy may be amended for lemmas that are used as
functional arguments, such as reflection or cancellation lemmas. Unfortunately
there is currently no easy way to tell Coq to use different defaults for
definitions and lemmas, so MathComp sticks to the on-demand default, as there
are significantly more lemmas than definition, and use the Prenex Implicits to
redress matters in bulk for definitions. However, this is not completely
systematic, and is sometimes omitted for constants that are not used as
functional arguments in the library, or inside the sections in which the
definition occur, since such commands need to be repeated after the section is
closed. Since Arguments commands should document the intended constant usage as
best as possible, they should follow the implicits policy - even in cases such
as this where the Prenex Implicits had been skipped.

6 files changed, 54 insertions, 56 deletions

diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index 6752623..a657fa5 100644
--- a/mathcomp/character/character.v
+++ b/mathcomp/character/character.v
@@ -544,7 +544,7 @@ Notation xcfun_r A := (xcfun_r_head tt A).
 Notation "phi .[ A ]" := (xcfun phi A) : cfun_scope.
 
 Definition pred_Nirr gT B := #|@classes gT B|.-1.
-Arguments pred_Nirr _ _%g.
+Arguments pred_Nirr {gT} B%g.
 Notation Nirr G := (pred_Nirr G).+1.
 Notation Iirr G := 'I_(Nirr G).
 
@@ -587,7 +587,7 @@ Proof. by apply: onW_bij; exists irr_of_socle. Qed.
 End IrrClassDef.
 
 Prenex Implicits socle_of_IirrK irr_of_socleK.
-Arguments socle_of_Iirr _ _%R.
+Arguments socle_of_Iirr {gT G%G} i%R.
 
 Notation "''Chi_' i" := (irr_repr (socle_of_Iirr i))
   (at level 8, i at level 2, format "''Chi_' i").
@@ -598,7 +598,7 @@ Definition irr_def gT B : (Nirr B).-tuple 'CF(B) :=
    [tuple of mkseq irr_of (Nirr B)].
 Definition irr := locked_with irr_key irr_def.
 
-Arguments irr _ _%g.
+Arguments irr {gT} B%g.
 
 Notation "''chi_' i" :=  (tnth (irr _) i%R)
   (at level 8, i at level 2, format "''chi_' i") : ring_scope.
@@ -621,7 +621,7 @@ Proof. by move/Iirr1_neq0; exists (inord 1). Qed.
 
 Lemma irrRepr i : cfRepr 'Chi_i = 'chi_i.
 Proof.
-rewrite [irr]unlock (tnth_nth 0) nth_mkseq // -[<<G>>]/(gval _) genGidG.
+rewrite [@irr]unlock (tnth_nth 0) nth_mkseq // -[<<G>>]/(gval _) genGidG.
 by rewrite cfRes_id inord_val.
 Qed.
 
@@ -816,7 +816,7 @@ Qed.
 
 End IrrClass.
 
-Arguments cfReg _ _%g.
+Arguments cfReg {gT} B%g.
 Prenex Implicits cfIirr.
 Arguments irr_inj {gT G} [x1 x2].
 
@@ -1334,7 +1334,7 @@ Qed.
 
 End OrthogonalityRelations.
 
-Arguments character_table _ _%g.
+Arguments character_table {gT} G%g.
 
 Section InnerProduct.
 
@@ -1565,7 +1565,7 @@ Qed.
 
 End IrrConstt.
 
-Arguments irr_constt _ _%g _%CF.
+Arguments irr_constt {gT B%g} phi%CF.
 
 Section Kernel.
 
@@ -1733,7 +1733,7 @@ Qed.
 
 End Restrict.
 
-Arguments Res_Iirr _ _%g _%g _%R.
+Arguments Res_Iirr {gT A%g} B%g i%R.
 
 Section MoreConstt.
 
@@ -1870,7 +1870,7 @@ Proof. by apply/eqP; rewrite isom_Iirr_eq0. Qed.
 
 End Isom.
 
-Arguments isom_Iirr_inj [aT rT G f R] isoGR [x1 x2].
+Arguments isom_Iirr_inj {aT rT G f R} isoGR [i1 i2] : rename.
 
 Section IsomInv.
 
@@ -1938,7 +1938,7 @@ Qed.
 
 End Sdprod.
 
-Arguments sdprod_Iirr_inj [gT K H G] defG [x1 x2].
+Arguments sdprod_Iirr_inj {gT K H G} defG [i1 i2] : rename.
 
 Section DProd.
 
@@ -2089,7 +2089,7 @@ Proof. by apply/(canLR dprod_IirrK); rewrite dprod_Iirr0. Qed.
 
 End DProd.
 
-Arguments dprod_Iirr_inj [gT G K H] KxH [x1 x2].
+Arguments dprod_Iirr_inj {gT G K H} KxH [i1 i2] : rename.
 
 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.
 
-Arguments aut_Iirr_inj [gT G] u [x1 x2].
+Arguments aut_Iirr_inj {gT G} u [i1 i2] : rename.
 
 Section Coset.
 
@@ -2993,4 +2993,4 @@ Proof. by move/cfker_Ind->; rewrite ?irr_neq0 ?irr_char. Qed.
 
 End Induced.
 
-Arguments Ind_Iirr _ _%g _%g _%R.
\ No newline at end of file
+Arguments Ind_Iirr {gT A%g} B%g i%R.
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index ac3e5bc..7b2b90d 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -392,14 +392,13 @@ End Defs.
 
 Bind Scope cfun_scope with classfun.
 
-Arguments classfun _ _%g.
-Arguments classfun_on _ _%g _%g.
-Arguments cfun_indicator _ _%g.
-Arguments cfAut _ _%g _ _%CF.
-Arguments cfReal _ _%g _%CF.
-Arguments cfdot _ _%g _%CF _%CF.
-Arguments cfdotr_head _ _%g _ _%CF _%CF.
-Arguments cfdotr_head _ _%g _ _%CF.
+Arguments classfun {gT} B%g.
+Arguments classfun_on {gT} B%g A%g.
+Arguments cfun_indicator {gT} B%g.
+Arguments cfAut {gT B%g} u phi%CF.
+Arguments cfReal {gT B%g} phi%CF.
+Arguments cfdot {gT B%g} phi%CF psi%CF.
+Arguments cfdotr_head {gT B%g} k psi%CF phi%CF.
 
 Notation "''CF' ( G )" := (classfun G) : type_scope.
 Notation "''CF' ( G )" := (@fullv _ (cfun_vectType G)) : vspace_scope.
@@ -452,12 +451,12 @@ End Predicates.
 (* Outside section so the nosimpl does not get "cooked" out. *)
 Definition orthogonal gT D S1 S2 := nosimpl (@ortho_rec gT D S1 S2).
 
-Arguments cfker _ _%g _%CF.
-Arguments cfaithful _ _%g _%CF.
-Arguments orthogonal _ _%g _%CF _%CF.
-Arguments pairwise_orthogonal _ _%g _%CF.
-Arguments orthonormal _ _%g _%CF.
-Arguments isometry _ _ _%g _%g _%CF.
+Arguments cfker {gT D%g} phi%CF.
+Arguments cfaithful {gT D%g} phi%CF.
+Arguments orthogonal {gT D%g} S1%CF S2%CF.
+Arguments pairwise_orthogonal {gT D%g} S%CF.
+Arguments orthonormal {gT D%g} S%CF.
+Arguments isometry {gT rT D%g R%g} tau%CF.
 
 Notation "{ 'in' CFD , 'isometry' tau , 'to' CFR }" :=
     (isometry_from_to (mem CFD) tau (mem CFR))
@@ -756,7 +755,7 @@ Proof. by []. Qed.
 
 End ClassFun.
 
-Arguments classfun_on _ _%g _%g.
+Arguments classfun_on {gT} B%g A%g.
 Notation "''CF' ( G , A )" := (classfun_on G A) : ring_scope.
 
 Arguments cfun_onP {gT G A phi}.
@@ -1394,7 +1393,7 @@ Canonical cfRes_lrmorphism := [lrmorphism of cfRes].
 
 End Restrict.
 
-Arguments cfRes _ _%g _%g _%CF.
+Arguments cfRes {gT} A%g {B%g} phi%CF.
 Notation "''Res[' H , G ]" := (@cfRes _ H G) (only parsing) : ring_scope.
 Notation "''Res[' H ]" := 'Res[H, _] : ring_scope.
 Notation "''Res'" := 'Res[_] (only parsing) : ring_scope.
@@ -1621,7 +1620,7 @@ Proof. exact: cforder_inj_rmorph cfIsom_inj. Qed.
 
 End InvMorphism.
 
-Arguments cfIsom_inj [aT rT G f R] isoGR [x1 x2].
+Arguments cfIsom_inj {aT rT G f R} isoGR [phi1 phi2] : rename.
 
 Section Coset.
 
@@ -1727,9 +1726,8 @@ Proof. by move=> nsBG kerH; rewrite -cfMod_eq1 // cfQuoK. Qed.
 
 End Coset.
 
-Arguments cfQuo _ _%G _%g _%CF.
-Arguments cfMod _ _%G _%g _%CF.
-Prenex Implicits cfMod.
+Arguments cfQuo {gT G%G} B%g phi%CF.
+Arguments cfMod {gT G%G B%g} phi%CF.
 Notation "phi / H" := (cfQuo H phi) : cfun_scope.
 Notation "phi %% H" := (@cfMod _ _ H phi) : cfun_scope.
 
@@ -2327,7 +2325,7 @@ Qed.
 
 End Induced.
 
-Arguments cfInd _ _%g _%g _%CF.
+Arguments cfInd {gT} B%g {A%g} phi%CF.
 Notation "''Ind[' G , H ]" := (@cfInd _ G H) (only parsing) : ring_scope.
 Notation "''Ind[' G ]" := 'Ind[G, _] : ring_scope.
 Notation "''Ind'" := 'Ind[_] (only parsing) : ring_scope.
@@ -2489,7 +2487,7 @@ End FieldAutomorphism.
 
 Arguments cfAutK u {gT G}.
 Arguments cfAutVK u {gT G}.
-Arguments cfAut_inj u [gT G x1 x2].
+Arguments cfAut_inj u {gT G} [phi1 phi2] : rename.
 
 Definition conj_cfRes := cfAutRes conjC.
 Definition cfker_conjC := cfker_aut conjC.
diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v
index ffa9696..80d5cc5 100644
--- a/mathcomp/character/inertia.v
+++ b/mathcomp/character/inertia.v
@@ -567,9 +567,9 @@ Qed.
 
 End Inertia.
 
-Arguments inertia _ _%g _%CF.
-Arguments cfclass _ _%g _%CF _%g.
-Arguments conjg_Iirr_inj [gT H] y [x1 x2].
+Arguments inertia {gT B%g} phi%CF.
+Arguments cfclass {gT A%g} phi%CF B%g.
+Arguments conjg_Iirr_inj {gT H} y [i1 i2] : rename.
 
 Notation "''I[' phi ] " := (inertia phi) : group_scope.
 Notation "''I[' phi ] " := (inertia_group phi) : Group_scope.
diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v
index f0553f2..3c2b0d6 100644
--- a/mathcomp/character/integral_char.v
+++ b/mathcomp/character/integral_char.v
@@ -157,7 +157,7 @@ Canonical gring_irr_mode_unlockable := [unlockable fun gring_irr_mode].
 
 End GenericClassSums.
 
-Arguments gring_irr_mode _ _%G _%R _%g : extra scopes.
+Arguments gring_irr_mode {gT G%G} i%R _%g : extra scopes.
 
 Notation "''K_' i" := (gring_class_sum _ i)
   (at level 8, i at level 2, format "''K_' i") : ring_scope.
diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v
index b121f4c..69055d4 100644
--- a/mathcomp/character/mxabelem.v
+++ b/mathcomp/character/mxabelem.v
@@ -341,7 +341,7 @@ Proof. by move=> sHG; rewrite gacentE // setTI afix_repr. Qed.
 
 End FinFieldRepr.
 
-Arguments rowg_mx _ _ _%g.
+Arguments rowg_mx {F n%N} L%g.
 Notation "''Zm'" := (scale_action _ _ _) (at level 8) : action_scope.
 Notation "''Zm'" := (scale_groupAction _ _ _) : groupAction_scope.
 
@@ -406,7 +406,7 @@ Open Scope abelem_scope.
 
 Definition abelem_dim' (gT : finGroupType) (E : {set gT}) :=
   (logn (pdiv #|E|) #|E|).-1.
-Arguments abelem_dim' _ _%g.
+Arguments abelem_dim' {gT} E%g.
 Notation "''dim' E" := (abelem_dim' E).+1
   (at level 10, E at level 8, format "''dim'  E") : abelem_scope.
 
diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v
index 6859168..560b61d 100644
--- a/mathcomp/character/mxrepresentation.v
+++ b/mathcomp/character/mxrepresentation.v
@@ -814,10 +814,10 @@ End Regular.
 
 End RingRepr.
 
-Arguments mx_representation _ _ _%g _%N.
-Arguments mx_repr _ _ _%g _%N _.
-Arguments group_ring _ _ _%g.
-Arguments regular_repr _ _ _%g.
+Arguments mx_representation R {gT} G%g n%N.
+Arguments mx_repr {R gT} G%g {n%N} r.
+Arguments group_ring R {gT} G%g.
+Arguments regular_repr R {gT} G%g.
 
 Arguments centgmxP {R gT G n rG f}.
 Arguments rkerP {R gT G n rG x}.
@@ -2377,8 +2377,8 @@ 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}.
+Arguments val_submod_inj {n U m} [W1 W2] : rename.
+Arguments val_factmod_inj {n U m} [W1 W2] : rename.
 
 Section Proper.
 
@@ -4652,10 +4652,10 @@ End LinearIrr.
 
 End FieldRepr.
 
-Arguments rfix_mx _ _ _%g _%N _ _%g.
-Arguments gset_mx _ _ _%g _%g.
-Arguments classg_base _ _ _%g _%g : extra scopes.
-Arguments irrType _ _ _%g _%g : extra scopes.
+Arguments rfix_mx {F gT G%g n%N} rG H%g.
+Arguments gset_mx F {gT} G%g A%g.
+Arguments classg_base F {gT} G%g _%g : extra scopes.
+Arguments irrType F {gT} G%g.
 
 Arguments mxmoduleP {F gT G n rG m U}.
 Arguments envelop_mxP {F gT G n rG A}.
@@ -4671,16 +4671,16 @@ 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}.
+Arguments val_submod_inj {F n U m} [W1 W2] : rename.
+Arguments val_factmod_inj {F n U m} [W1 W2] : rename.
 
 Notation "'Cl" := (Clifford_action _) : action_scope.
 
 Bind Scope irrType_scope with socle_sort.
 Notation "[ 1 sG ]" := (principal_comp sG) : irrType_scope.
-Arguments irr_degree _ _ _%G _ _%irr.
-Arguments irr_repr _ _ _%G _ _%irr _%g : extra scopes.
-Arguments irr_mode _ _ _%G _ _%irr _%g : extra scopes.
+Arguments irr_degree {F gT G%G sG} i%irr.
+Arguments irr_repr [F gT G%G sG] i%irr _%g : extra scopes.
+Arguments irr_mode [F gT G%G sG] i%irr z%g : rename.
 Notation "''n_' i" := (irr_degree i) : group_ring_scope.
 Notation "''R_' i" := (Wedderburn_subring i) : group_ring_scope.
 Notation "''e_' i" := (Wedderburn_id i) : group_ring_scope.