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, 24 insertions, 26 deletions

diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v
index ffea847..9a8032d 100644
--- a/mathcomp/fingroup/action.v
+++ b/mathcomp/fingroup/action.v
@@ -148,10 +148,10 @@ End ActionDef.
 (* Need to close the Section here to avoid re-declaring all Argument Scopes *)
 Delimit Scope action_scope with act.
 Bind Scope action_scope with action.
-Arguments act_morph _ _%g _ _ _%g : extra scopes.
-Arguments is_action _ _%g _ _.
-Arguments act _ _%g _%type _%act _%g _%g.
-Arguments clone_action _ _%g _%type _%act _.
+Arguments act_morph {aT rT%type} to x%g.
+Arguments is_action {aT} D%g {rT} to.
+Arguments act {aT D%g rT%type} to%act x%g a%g : rename.
+Arguments clone_action [aT D%g rT%type to%act] _.
 
 Notation "{ 'action' aT &-> T }" := (action [set: aT] T)
   (at level 0, format "{ 'action'  aT  &->  T }") : type_scope.
@@ -210,15 +210,15 @@ Definition faithful A S to := A :&: astab S to \subset [1].
 
 End ActionDefs.
 
-Arguments setact _ _%g _ _%act _%g _%g.
-Arguments orbit _ _%g _ _%act _%g _%g.
-Arguments amove _ _%g _ _%act _%g _%g _%g.
-Arguments afix _ _%g _ _%act _%g.
-Arguments astab _ _%g _ _%g _%act.
-Arguments astabs _ _%g _ _%g _%act.
-Arguments acts_on _ _%g _ _%g _%g _%act.
-Arguments atrans _ _%g _ _%g _%g _%act.
-Arguments faithful _ _%g _ _%g _%g _%act.
+Arguments setact {aT D%g rT} to%act S%g a%g.
+Arguments orbit {aT D%g rT} to%act A%g x%g.
+Arguments amove {aT D%g rT} to%act A%g x%g y%g.
+Arguments afix {aT D%g rT} to%act A%g.
+Arguments astab {aT D%g rT} S%g to%act.
+Arguments astabs {aT D%g rT} S%g to%act.
+Arguments acts_on {aT D%g rT} A%g S%g to%act.
+Arguments atrans {aT D%g rT} A%g S%g to%act.
+Arguments faithful {aT D%g rT} A%g S%g to%act.
 
 Notation "to ^*" := (setact to) (at level 2, format "to ^*") : fun_scope.
 
@@ -482,9 +482,7 @@ End Reindex.
 
 End RawAction.
 
-(* Warning: this directive depends on names of bound variables in the *)
-(* definition of injective, in ssrfun.v.                              *)
-Arguments act_inj {aT D rT} to _ [x1 x2].
+Arguments act_inj {aT D rT} to a [x1 x2] : rename.
 
 Notation "to ^*" := (set_action to) : action_scope.
 
@@ -874,7 +872,7 @@ Qed.
 
 End PartialAction.
 
-Arguments orbit_transversal _ _%g _ _%act _%g _%g.
+Arguments orbit_transversal {aT D%g rT} to%act A%g S%g.
 Arguments orbit_in_eqP {aT D rT to G x y}.
 Arguments orbit1P {aT D rT to G x}.
 Arguments contra_orbit [aT D rT] to G [x y].
@@ -1741,7 +1739,7 @@ Qed.
 
 End AutIn.
 
-Arguments Aut_in _ _%g _%g.
+Arguments Aut_in {gT} A%g B%g.
 
 Section InjmAutIn.
 
@@ -1818,9 +1816,9 @@ End GroupAction.
 Delimit Scope groupAction_scope with gact.
 Bind Scope groupAction_scope with groupAction.
 
-Arguments is_groupAction _ _ _%g _%g _%act.
-Arguments groupAction _ _ _%g _%g.
-Arguments gact _ _ _%g _%g _%gact.
+Arguments is_groupAction {aT rT D%g} R%g to%act.
+Arguments groupAction {aT rT} D%g R%g.
+Arguments gact {aT rT D%g R%g} to%gact : rename.
 
 Notation "[ 'groupAction' 'of' to ]" :=
      (clone_groupAction (@GroupAction _ _ _ _ to))
@@ -1847,9 +1845,9 @@ Definition acts_irreducibly A S to :=
 
 End GroupActionDefs.
 
-Arguments gacent _ _ _%g _%g _%gact _%g.
-Arguments acts_on_group _ _ _%g _%g _%g _%g _%gact.
-Arguments acts_irreducibly _ _ _%g _%g _%g _%g _%gact.
+Arguments gacent {aT rT D%g R%g} to%gact A%g.
+Arguments acts_on_group {aT rT D%g R%g} A%g S%g to%gact.
+Arguments acts_irreducibly {aT rT D%g R%g} A%g S%g to%gact.
 
 Notation "''C_' ( | to ) ( A )" := (gacent to A)
   (at level 8, format "''C_' ( | to ) ( A )") : group_scope.
@@ -2705,8 +2703,8 @@ Canonical aut_groupAction := GroupAction autact_is_groupAction.
 
 End AutAct.
 
-Arguments aut_action _ _%g.
-Arguments aut_groupAction _ _%g.
+Arguments aut_action {gT} G%g.
+Arguments aut_groupAction {gT} G%g.
 Notation "[ 'Aut' G ]" := (aut_action G) : action_scope.
 Notation "[ 'Aut' G ]" := (aut_groupAction G) : groupAction_scope.