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.

1 files changed, 18 insertions, 18 deletions

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.