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.

13 files changed, 88 insertions, 92 deletions

diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v
index 5f1a013..746898f 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -111,16 +111,16 @@ Definition gen_rank A := #|[arg min_(B < A | <<B>> == A) #|B|]|.
 
 End AbelianDefs.
 
-Arguments exponent _ _%g.
-Arguments abelem _ _%N _%g.
-Arguments is_abelem _ _%g.
-Arguments pElem _ _%N _%g.
-Arguments pnElem _ _%N _%N _%g.
-Arguments nElem _ _%N _%g.
-Arguments pmaxElem _ _%N _%g.
-Arguments p_rank _ _%N _%g.
-Arguments rank _ _%g.
-Arguments gen_rank _ _%g.
+Arguments exponent {gT} A%g.
+Arguments abelem {gT} p%N A%g.
+Arguments is_abelem {gT} A%g.
+Arguments pElem {gT} p%N A%g.
+Arguments pnElem {gT} p%N n%N A%g.
+Arguments nElem {gT} n%N A%g.
+Arguments pmaxElem {gT} p%N A%g.
+Arguments p_rank {gT} p%N A%g.
+Arguments rank {gT} A%g.
+Arguments gen_rank {gT} A%g.
 
 Notation "''Ldiv_' n ()" := (Ldiv _ n)
   (at level 8, n at level 2, format "''Ldiv_' n ()") : group_scope.
@@ -192,10 +192,10 @@ Qed.
 
 End Functors.
 
-Arguments Ohm _%N _ _%g.
-Arguments Ohm_group _%N _ _%g.
-Arguments Mho _%N _ _%g.
-Arguments Mho_group _%N _ _%g.
+Arguments Ohm n%N {gT} A%g.
+Arguments Ohm_group n%N {gT} A%g.
+Arguments Mho n%N {gT} A%g.
+Arguments Mho_group n%N {gT} A%g.
 Arguments OhmPredP {n gT x}.
 
 Notation "''Ohm_' n ( G )" := (Ohm n G)
@@ -2023,8 +2023,8 @@ Qed.
 
 End AbelianStructure.
 
-Arguments abelian_type {_} _%g.
-Arguments homocyclic {_} _%g.
+Arguments abelian_type {gT} A%g.
+Arguments homocyclic {gT} A%g.
 
 Section IsogAbelian.
 
diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v
index 1c804cc..10cbbaa 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.
 
-Arguments burnside_formula [gT].
+Arguments burnside_formula {gT}.
 
 Section colouring.
 
diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v
index 98434ba..88774db 100644
--- a/mathcomp/solvable/center.v
+++ b/mathcomp/solvable/center.v
@@ -56,11 +56,11 @@ Canonical center_group (G : {group gT}) : {group gT} :=
 
 End Defs.
 
-Arguments center _ _%g.
+Arguments center {gT} A%g.
 Notation "''Z' ( A )" := (center A) : group_scope.
 Notation "''Z' ( H )" := (center_group H) : Group_scope.
 
-Lemma morphim_center : GFunctor.pcontinuous center.
+Lemma morphim_center : GFunctor.pcontinuous (@center).
 Proof. by move=> gT rT G D f; apply: morphim_subcent. Qed.
 
 Canonical center_igFun := [igFun by fun _ _ => subsetIl _ _ & morphim_center].
diff --git a/mathcomp/solvable/commutator.v b/mathcomp/solvable/commutator.v
index dcd53ce..7895116 100644
--- a/mathcomp/solvable/commutator.v
+++ b/mathcomp/solvable/commutator.v
@@ -33,7 +33,7 @@ Definition derived_at_rec n (gT : finGroupType) (A : {set gT}) :=
 (* "cooking" destroys it.                                                    *)
 Definition derived_at := nosimpl derived_at_rec.
 
-Arguments derived_at _%N _ _%g.
+Arguments derived_at n%N {gT} A%g.
 Notation "G ^` ( n )" := (derived_at n G) : group_scope.
 
 Section DerivedBasics.
@@ -354,7 +354,7 @@ End Commutator_properties.
 
 Arguments derG1P {gT G}.
 
-Lemma der_cont n : GFunctor.continuous (derived_at n).
+Lemma der_cont n : GFunctor.continuous (@derived_at n).
 Proof. by move=> aT rT G f; rewrite morphim_der. Qed.
 
 Canonical der_igFun n := [igFun by der_sub^~ n & der_cont n].
diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v
index 046f4a2..e370a7e 100644
--- a/mathcomp/solvable/cyclic.v
+++ b/mathcomp/solvable/cyclic.v
@@ -289,9 +289,9 @@ Proof. by rewrite /order => /(<[a]> =P _)->. Qed.
 
 End Cyclic.
 
-Arguments cyclic {_} _%g.
-Arguments generator {_}_%g _%g.
-Arguments expg_invn {_} _%g _%N.
+Arguments cyclic {gT} A%g.
+Arguments generator {gT} A%g a%g.
+Arguments expg_invn {gT} A%g k%N.
 Arguments cyclicP {gT A}.
 Prenex Implicits cyclic Zpm.
 
@@ -556,7 +556,7 @@ Qed.
 
 End Metacyclic.
 
-Arguments metacyclic {_} _%g.
+Arguments metacyclic {gT} A%g.
 Arguments metacyclicP {gT A}.
 
 (* Automorphisms of cyclic groups. *)
diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v
index f7edfc9..01ba8f3 100644
--- a/mathcomp/solvable/frobenius.v
+++ b/mathcomp/solvable/frobenius.v
@@ -98,15 +98,15 @@ Variant has_Frobenius_action G H : Prop :=
 
 End Definitions.
 
-Arguments semiregular _ _%g _%g.
-Arguments semiprime _ _%g _%g.
-Arguments normedTI _ _%g _%g _%g.
-Arguments Frobenius_group_with_complement _ _%g _%g.
-Arguments Frobenius_group _ _%g.
-Arguments Frobenius_group_with_kernel _ _%g _%g.
-Arguments Frobenius_group_with_kernel_and_complement _ _%g _%g _%g.
-Arguments Frobenius_action _ _%g _%g _ _%g _%act.
-Arguments has_Frobenius_action _ _%g _%g.
+Arguments semiregular {gT} K%g H%g.
+Arguments semiprime {gT} K%g H%g.
+Arguments normedTI {gT} A%g G%g L%g.
+Arguments Frobenius_group_with_complement {gT} G%g H%g.
+Arguments Frobenius_group {gT} G%g.
+Arguments Frobenius_group_with_kernel {gT} G%g K%g.
+Arguments Frobenius_group_with_kernel_and_complement {gT} G%g K%g H%g.
+Arguments Frobenius_action {gT} G%g H%g {sT} S%g to%act.
+Arguments has_Frobenius_action {gT} G%g H%g.
 
 Notation "[ 'Frobenius' G 'with' 'complement' H ]" :=
   (Frobenius_group_with_complement G H)
diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v
index a1830b9..3e99bfb 100644
--- a/mathcomp/solvable/gseries.v
+++ b/mathcomp/solvable/gseries.v
@@ -71,16 +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 invariant_factor _ _%g _%g _%g.
-Arguments stable_factor _ _%g _%g _%g.
-Arguments central_factor _ _%g _%g _%g.
-Arguments maximal {_} _%g _%g.
-Arguments maximal_eq _ _%g _%g.
-Arguments maxnormal _ _%g _%g _%g.
-Arguments minnormal _ _%g _%g.
-Arguments simple {_} _%g.
-Arguments chief_factor _ _%g _%g _%g.
+Arguments subnormal {gT} A%g B%g.
+Arguments invariant_factor {gT} A%g B%g C%g.
+Arguments stable_factor {gT} A%g V%g U%g.
+Arguments central_factor {gT} A%g V%g U%g.
+Arguments maximal {gT} A%g B%g.
+Arguments maximal_eq {gT} A%g B%g.
+Arguments maxnormal {gT} A%g B%g U%g.
+Arguments minnormal {gT} A%g B%g.
+Arguments simple {gT} A%g.
+Arguments chief_factor {gT} A%g V%g U%g.
 
 Notation "H <|<| G" := (subnormal H G)
   (at level 70, no associativity) : group_scope.
@@ -94,7 +94,7 @@ Notation "A .-central" := (central_factor A)
 Notation "G .-chief" := (chief_factor G)
   (at level 2, format "G .-chief") : group_rel_scope.
 
-Arguments group_rel_of _ _%group_rel_scope _%G _%G : extra scopes.
+Arguments group_rel_of {gT} r%group_rel_scope _%G _%G : extra scopes.
 
 Notation "r .-series" := (path (rel_of_simpl_rel (group_rel_of r)))
   (at level 2, format "r .-series") : group_scope.
diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v
index 91cc709..bda66bd 100644
--- a/mathcomp/solvable/jordanholder.v
+++ b/mathcomp/solvable/jordanholder.v
@@ -475,8 +475,8 @@ Qed.
 
 End StableCompositionSeries.
 
-Arguments maxainv _ _ _%G _%G _%gact _%g _%g.
-Arguments asimple _ _ _%G _%G _%gact _%g.
+Arguments maxainv {aT rT D%G A%G} to%gact B%g C%g.
+Arguments asimple {aT rT D%G A%G} to%gact K%g.
 
 Section StrongJordanHolder.
 
diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v
index 5f7a9ed..781abbe 100644
--- a/mathcomp/solvable/maximal.v
+++ b/mathcomp/solvable/maximal.v
@@ -102,16 +102,14 @@ Definition SCN_at n B := [set A in SCN B | n <= 'r(A)].
 
 End Defs.
 
-Arguments charsimple _ _%g.
-Arguments Frattini _ _%g.
-Arguments Fitting _ _%g.
-Arguments critical _ _%g _%g.
-Arguments special _ _%g.
-Arguments extraspecial _ _%g.
-Arguments SCN _ _%g.
-Arguments SCN_at _ _%N _%g.
-
-Prenex Implicits maximal simple charsimple critical special extraspecial.
+Arguments charsimple {gT} A%g.
+Arguments Frattini {gT} A%g.
+Arguments Fitting {gT} A%g.
+Arguments critical {gT} A%g B%g.
+Arguments special {gT} A%g.
+Arguments extraspecial {gT} A%g.
+Arguments SCN {gT} B%g.
+Arguments SCN_at {gT} n%N B%g.
 
 Notation "''Phi' ( A )" := (Frattini A)
   (at level 8, format "''Phi' ( A )") : group_scope.
@@ -459,7 +457,7 @@ Section FittingFun.
 
 Implicit Types gT rT : finGroupType.
 
-Lemma morphim_Fitting : GFunctor.pcontinuous Fitting.
+Lemma morphim_Fitting : GFunctor.pcontinuous (@Fitting).
 Proof.
 move=> gT rT G D f; apply: Fitting_max.
   by rewrite morphim_normal ?Fitting_normal.
diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v
index d631919..aee3113 100644
--- a/mathcomp/solvable/nilpotent.v
+++ b/mathcomp/solvable/nilpotent.v
@@ -52,8 +52,8 @@ Definition lower_central_at n := lower_central_at_rec n.-1.
 (* "cooking" destroys it.                                                     *)
 Definition upper_central_at := nosimpl upper_central_at_rec.
 
-Arguments lower_central_at _%N _ _%g.
-Arguments upper_central_at _%N _ _%g.
+Arguments lower_central_at n%N {gT} A%g.
+Arguments upper_central_at n%N {gT} A%g.
 
 Notation "''L_' n ( G )" := (lower_central_at n G)
   (at level 8, n at level 2, format "''L_' n ( G )") : group_scope.
@@ -75,9 +75,9 @@ Definition solvable :=
 
 End PropertiesDefs.
 
-Arguments nilpotent {_} _%g.
-Arguments nil_class {_} _%g.
-Arguments solvable {_} _%g.
+Arguments nilpotent {gT} A%g.
+Arguments nil_class {gT} A%g.
+Arguments solvable {gT} A%g.
 
 Section NilpotentProps.
 
@@ -320,7 +320,7 @@ End LowerCentral.
 
 Notation "''L_' n ( G )" := (lower_central_at_group n G) : Group_scope.
 
-Lemma lcn_cont n : GFunctor.continuous (lower_central_at n).
+Lemma lcn_cont n : GFunctor.continuous (@lower_central_at n).
 Proof.
 case: n => //; elim=> // n IHn g0T h0T H phi.
 by rewrite !lcnSn morphimR ?lcn_sub // commSg ?IHn.
@@ -338,7 +338,7 @@ Implicit Type gT : finGroupType.
 Lemma ucn_pmap : exists hZ : GFunctor.pmap, @upper_central_at n = hZ.
 Proof.
 elim: n => [|n' [hZ defZ]]; first by exists trivGfun_pgFun.
-by exists [pgFun of center %% hZ]; rewrite /= -defZ.
+by exists [pgFun of @center %% hZ]; rewrite /= -defZ.
 Qed.
 
 (* Now extract all the intermediate facts of the last proof. *)
@@ -351,7 +351,7 @@ Canonical upper_central_at_group gT G := Group (@ucn_group_set gT G).
 Lemma ucn_sub gT (G : {group gT}) : 'Z_n(G) \subset G.
 Proof. by have [hZ ->] := ucn_pmap; apply: gFsub. Qed.
 
-Lemma morphim_ucn : GFunctor.pcontinuous (upper_central_at n).
+Lemma morphim_ucn : GFunctor.pcontinuous (@upper_central_at n).
 Proof. by have [hZ ->] := ucn_pmap; apply: pmorphimF. Qed.
 
 Canonical ucn_igFun := [igFun by ucn_sub & morphim_ucn].
diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v
index 6c02e7b..d62154f 100644
--- a/mathcomp/solvable/pgroup.v
+++ b/mathcomp/solvable/pgroup.v
@@ -83,15 +83,15 @@ Definition Sylow A B := p_group B && Hall A B.
 
 End PgroupDefs.
 
-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 pHall _ _%N _%g _%g.
-Arguments Syl _ _%N _%g.
-Arguments Sylow {_} _%g _%g.
+Arguments pgroup {gT} pi%N A%g.
+Arguments psubgroup {gT} pi%N A%g B%g.
+Arguments p_group {gT} A%g.
+Arguments p_elt {gT} pi%N x.
+Arguments constt {gT} x%g pi%N.
+Arguments Hall {gT} A%g B%g.
+Arguments pHall {gT} pi%N A%g B%g.
+Arguments Syl {gT} p%N A%g.
+Arguments Sylow {gT} A%g B%g.
 
 Notation "pi .-group" := (pgroup pi)
   (at level 2, format "pi .-group") : group_scope.
@@ -861,8 +861,8 @@ Canonical pcore_group : {group gT} := Eval hnf in [group of pcore].
 
 End PcoreDef.
 
-Arguments pcore _ _%N _%g.
-Arguments pcore_group _ _%N _%G.
+Arguments pcore pi%N {gT} A%g.
+Arguments pcore_group pi%N {gT} A%G.
 Notation "''O_' pi ( G )" := (pcore pi G)
   (at level 8, pi at level 2, format "''O_' pi ( G )") : group_scope.
 Notation "''O_' pi ( G )" := (pcore_group pi G) : Group_scope.
@@ -884,7 +884,7 @@ Canonical pseries_group : {group gT} := group pseries_group_set.
 
 End PseriesDefs.
 
-Arguments pseries _ _%SEQ _%g.
+Arguments pseries pis%SEQ {gT} _%g.
 Local Notation ConsPred p := (@Cons nat_pred p%N) (only parsing).
 Notation "''O_{' p1 , .. , pn } ( A )" :=
   (pseries (ConsPred p1 .. (ConsPred pn [::]) ..) A)
@@ -977,7 +977,7 @@ Section MorphPcore.
 
 Implicit Types (pi : nat_pred) (gT rT : finGroupType).
 
-Lemma morphim_pcore pi : GFunctor.pcontinuous (pcore pi).
+Lemma morphim_pcore pi : GFunctor.pcontinuous (@pcore pi).
 Proof.
 move=> gT rT D G f; apply/bigcapsP=> M /normal_sub_max_pgroup; apply.
   by rewrite morphim_pgroup ?pcore_pgroup.
@@ -1054,7 +1054,7 @@ Lemma pseries_rcons pi pis gT (A : {set gT}) :
 Proof. by rewrite /pseries rev_rcons. Qed.
 
 Lemma pseries_subfun pis :
-   GFunctor.closed (pseries pis) /\  GFunctor.pcontinuous (pseries pis).
+   GFunctor.closed (@pseries pis) /\  GFunctor.pcontinuous (@pseries pis).
 Proof.
 elim/last_ind: pis => [|pis pi [sFpi fFpi]].
   by split=> [gT G | gT rT D G f]; rewrite (sub1G, morphim1).
@@ -1064,13 +1064,13 @@ split=> [gT G | gT rT D G f]; rewrite !pseries_rcons ?(pcore_mod_sub F) //.
 exact: (morphim_pcore_mod F).
 Qed.
 
-Lemma pseries_sub pis : GFunctor.closed (pseries pis).
+Lemma pseries_sub pis : GFunctor.closed (@pseries pis).
 Proof. by case: (pseries_subfun pis). Qed.
 
-Lemma morphim_pseries pis : GFunctor.pcontinuous (pseries pis).
+Lemma morphim_pseries pis : GFunctor.pcontinuous (@pseries pis).
 Proof. by case: (pseries_subfun pis). Qed.
 
-Lemma pseriesS pis : GFunctor.hereditary (pseries pis).
+Lemma pseriesS pis : GFunctor.hereditary (@pseries pis).
 Proof. exact: (morphim_pseries pis). Qed.
 
 Canonical pseries_igFun pis := [igFun by pseries_sub pis & morphim_pseries pis].
@@ -1149,7 +1149,7 @@ apply: (quotient_inj nH2H).
   by apply/andP; rewrite /= -cats1 pseries_sub_catl pseries_norm2.
 rewrite /= quotient_pseries /= -IHpi -rcons_cat.
 rewrite -[G / _ / _](morphim_invm inj_f) //= {2}im_f //.
-rewrite -(@injmF [igFun of pcore pi]) /= ?injm_invm ?im_f // -quotient_pseries.
+rewrite -(@injmF [igFun of @pcore pi]) /= ?injm_invm ?im_f // -quotient_pseries.
 by rewrite -im_f ?morphim_invm ?morphimS ?normal_sub.
 Qed.
 
diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v
index 58a5f20..fa27e75 100644
--- a/mathcomp/solvable/primitive_action.v
+++ b/mathcomp/solvable/primitive_action.v
@@ -43,14 +43,12 @@ Definition primitive :=
 
 End PrimitiveDef.
 
-Arguments imprimitivity_system _ _ _%g _%g _%act _%g.
-Arguments primitive _ _ _%g _%g _%act.
+Arguments imprimitivity_system {aT sT} A%g S%g to%act Q%g.
+Arguments primitive {aT sT} A%g S%g to%act.
 
 Notation "[ 'primitive' A , 'on' S | to ]" := (primitive A S to)
   (at level 0, format "[ 'primitive'  A ,  'on'  S  |  to ]") : form_scope.
 
-Prenex Implicits imprimitivity_system.
-
 Section Primitive.
 
 Variables (aT : finGroupType) (sT : finType).
@@ -183,9 +181,9 @@ Qed.
 
 End NTransitive.
 
-Arguments dtuple_on _ _%N _%g.
-Arguments ntransitive _ _ _%N _%g _%g _%act.
-Arguments n_act [gT sT] _ [n].
+Arguments dtuple_on {sT} n%N S%g.
+Arguments ntransitive {gT sT} n%N A%g S%g to%act.
+Arguments n_act {gT sT} to {n} t a.
 
 Notation "n .-dtuple ( S )" := (dtuple_on n S)
   (at level 8, format "n .-dtuple ( S )") : set_scope.
diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v
index f940ec9..a428c0d 100644
--- a/mathcomp/solvable/sylow.v
+++ b/mathcomp/solvable/sylow.v
@@ -535,7 +535,7 @@ Qed.
 
 End Zgroups.
 
-Arguments Zgroup {_} _%g.
+Arguments Zgroup {gT} A%g.
 
 Section NilPGroups.