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, 55 deletions

diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index 2501117..3fe8d01 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -2663,7 +2663,7 @@ Coercion GLval ph (u : GLtype ph) : 'M[R]_n.-1.+1 :=
 End FinUnitMatrix.
 
 Bind Scope group_scope with GLtype.
-Arguments GLval {_%N _ _} _%g.
+Arguments GLval {n%N R ph} u%g.
 
 Notation "{ ''GL_' n [ R ] }" := (GLtype n (Phant R))
   (at level 0, n at level 2, format "{ ''GL_' n [ R ] }") : type_scope.
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index af18125..c23d91c 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -216,9 +216,9 @@ Definition pinvmx : 'M_(n, m) :=
 
 End Defs.
 
-Arguments mxrank _%N _%N _%MS.
+Arguments mxrank {m%N n%N} A%MS.
 Local Notation "\rank A" := (mxrank A) : nat_scope.
-Arguments complmx _%N _%N _%MS.
+Arguments complmx {m%N n%N} A%MS.
 Local Notation "A ^C" := (complmx A) : matrix_set_scope.
 
 Definition submx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) =>
@@ -227,21 +227,21 @@ Fact submx_key : unit. Proof. by []. Qed.
 Definition submx := locked_with submx_key submx_def.
 Canonical submx_unlockable := [unlockable fun submx].
 
-Arguments submx {_%N _%N _%N} _%MS _%MS.
+Arguments submx {m1%N m2%N n%N} A%MS B%MS : rename.
 Local Notation "A <= B" := (submx A B) : matrix_set_scope.
 Local Notation "A <= B <= C" := ((A <= B) && (B <= C))%MS : matrix_set_scope.
 Local Notation "A == B" := (A <= B <= A)%MS : matrix_set_scope.
 
 Definition ltmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :=
   (A <= B)%MS && ~~ (B <= A)%MS.
-Arguments ltmx {_%N _%N _%N} _%MS _%MS.
+Arguments ltmx {m1%N m2%N n%N} A%MS B%MS.
 Local Notation "A < B" := (ltmx A B) : matrix_set_scope.
 
 Definition eqmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :=
   prod (\rank A = \rank B)
        (forall m3 (C : 'M_(m3, n)),
             ((A <= C) = (B <= C)) * ((C <= A) = (C <= B)))%MS.
-Arguments eqmx _%N _%N _%N _%MS _%MS.
+Arguments eqmx {m1%N m2%N n%N} A%MS B%MS.
 Local Notation "A :=: B" := (eqmx A B) : matrix_set_scope.
 
 Section LtmxIdentities.
@@ -296,7 +296,7 @@ Definition addsmx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) =>
 Fact addsmx_key : unit. Proof. by []. Qed.
 Definition addsmx := locked_with addsmx_key addsmx_def.
 Canonical addsmx_unlockable := [unlockable fun addsmx].
-Arguments addsmx {_%N _%N _%N} _%MS _%MS.
+Arguments addsmx {m1%N m2%N n%N} A%MS B%MS : rename.
 Local Notation "A + B" := (addsmx A B) : matrix_set_scope.
 Local Notation "\sum_ ( i | P ) B" := (\big[addsmx/0]_(i | P) B%MS)
   : matrix_set_scope.
@@ -330,8 +330,7 @@ Definition capmx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) =>
 Fact capmx_key : unit. Proof. by []. Qed.
 Definition capmx := locked_with capmx_key capmx_def.
 Canonical capmx_unlockable := [unlockable fun capmx].
-Arguments capmx _%N _%N _%N _%MS _%MS.
-Prenex Implicits capmx.
+Arguments capmx {m1%N m2%N n%N} A%MS B%MS : rename.
 Local Notation "A :&: B" := (capmx A B) : matrix_set_scope.
 Local Notation "\bigcap_ ( i | P ) B" := (\big[capmx/1%:M]_(i | P) B)
   : matrix_set_scope.
@@ -341,7 +340,7 @@ Definition diffmx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) =>
 Fact diffmx_key : unit. Proof. by []. Qed.
 Definition diffmx := locked_with diffmx_key diffmx_def.
 Canonical diffmx_unlockable := [unlockable fun diffmx].
-Arguments diffmx {_%N _%N _%N} _%MS _%MS.
+Arguments diffmx {m1%N m2%N n%N} A%MS B%MS : rename.
 Local Notation "A :\: B" := (diffmx A B) : matrix_set_scope.
 
 Definition proj_mx n (U V : 'M_n) : 'M_n := pinvmx (col_mx U V) *m col_mx U 0.
@@ -1725,7 +1724,7 @@ Inductive mxsum_spec n : forall m, 'M[F]_(m, n) -> nat -> Prop :=
  | ProperMxsum m1 m2 T1 T2 r1 r2 of
       @mxsum_spec n m1 T1 r1 & @mxsum_spec n m2 T2 r2
     : mxsum_spec (T1 + T2)%MS (r1 + r2)%N.
-Arguments mxsum_spec _%N _%N _%MS _%N.
+Arguments mxsum_spec {n%N m%N} T%MS r%N.
 
 Structure mxsum_expr m n := Mxsum {
   mxsum_val :> wrapped 'M_(m, n);
@@ -1995,16 +1994,16 @@ Arguments mxdirect_sumsE {F I P n S_}.
 Arguments eigenspaceP {F n g a m W}.
 Arguments eigenvalueP {F n g a}.
 
-Arguments mxrank {_ _%N _%N} _%MS.
-Arguments complmx {_ _%N _%N} _%MS.
-Arguments row_full _ _%N _%N _%MS.
-Arguments submx {_ _%N _%N _%N} _%MS _%MS.
-Arguments ltmx {_ _%N _%N _%N} _%MS _%MS.
-Arguments eqmx {_ _%N _%N _%N} _%MS _%MS.
-Arguments addsmx {_ _%N _%N _%N} _%MS _%MS.
-Arguments capmx {_ _%N _%N _%N} _%MS _%MS.
-Arguments diffmx _ _%N _%N _%N _%MS _%MS.
-Prenex Implicits genmx.
+Arguments mxrank {F m%N n%N} A%MS.
+Arguments complmx {F m%N n%N} A%MS.
+Arguments row_full {F m%N n%N} A%MS.
+Arguments submx {F m1%N m2%N n%N} A%MS B%MS : rename.
+Arguments ltmx {F m1%N m2%N n%N} A%MS B%MS.
+Arguments eqmx {F m1%N m2%N n%N} A%MS B%MS.
+Arguments addsmx {F m1%N m2%N n%N} A%MS B%MS : rename.
+Arguments capmx {F m1%N m2%N n%N} A%MS B%MS : rename.
+Arguments diffmx {F m1%N m2%N n%N} A%MS B%MS : rename.
+Arguments genmx {F m%N n%N} A%R : rename.
 Notation "\rank A" := (mxrank A) : nat_scope.
 Notation "<< A >>" := (genmx A) : matrix_set_scope.
 Notation "A ^C" := (complmx A) : matrix_set_scope.
@@ -2279,7 +2278,7 @@ Qed.
 Definition mulsmx m1 m2 n (R1 : 'A[F]_(m1, n)) (R2 : 'A_(m2, n)) :=
   (\sum_i <<R1 *m lin_mx (mulmxr (vec_mx (row i R2)))>>)%MS.
 
-Arguments mulsmx _%N _%N _%N _%MS _%MS.
+Arguments mulsmx {m1%N m2%N n%N} R1%MS R2%MS.
 
 Local Notation "R1 * R2" := (mulsmx R1 R2) : matrix_set_scope.
 
@@ -2589,15 +2588,15 @@ Qed.
 
 End MatrixAlgebra.
 
-Arguments mulsmx {_ _%N _%N _%N} _%MS _%MS.
-Arguments left_mx_ideal _ _%N _%N _%N _%MS _%MS.
-Arguments right_mx_ideal _ _%N _%N _%N _%MS _%MS.
-Arguments mx_ideal _ _%N _%N _%N _%MS _%MS.
-Arguments mxring_id _ _%N _%N _%R _%MS.
-Arguments has_mxring_id _ _%N _%N _%R _%MS : extra scopes.
-Arguments mxring _ _%N _%N _%MS.
-Arguments cent_mx _ _%N _%N _%MS.
-Arguments center_mx _ _%N _%N _%MS.
+Arguments mulsmx {F m1%N m2%N n%N} R1%MS R2%MS.
+Arguments left_mx_ideal {F m1%N m2%N n%N} R%MS S%MS : rename.
+Arguments right_mx_ideal {F m1%N m2%N n%N} R%MS S%MS : rename.
+Arguments mx_ideal {F m1%N m2%N n%N} R%MS S%MS : rename.
+Arguments mxring_id {F m%N n%N} R%MS e%R.
+Arguments has_mxring_id {F m%N n%N} R%MS.
+Arguments mxring {F m%N n%N} R%MS.
+Arguments cent_mx {F m%N n%N} R%MS.
+Arguments center_mx {F m%N n%N} R%MS.
 
 Notation "A \in R" := (submx (mxvec A) R) : matrix_set_scope.
 Notation "R * S" := (mulsmx R S) : matrix_set_scope.
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index 34174bf..929c313 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -146,9 +146,9 @@ End Polynomial.
 (* directives take effect.                                         *)
 Bind Scope ring_scope with poly_of.
 Bind Scope ring_scope with polynomial.
-Arguments polyseq _ _%R.
-Arguments poly_inj _ _%R _%R _.
-Arguments coefp_head _ _ _%N _%R.
+Arguments polyseq {R} p%R.
+Arguments poly_inj {R} [p1%R p2%R] : rename.
+Arguments coefp_head {R} h i%N p%R.
 Notation "{ 'poly' T }" := (poly_of (Phant T)).
 Notation coefp i := (coefp_head tt i).
 
@@ -2430,7 +2430,7 @@ Qed.
 
 End MapFieldPoly.
 
-Arguments map_poly_inj {F R} f [x1 x2].
+Arguments map_poly_inj {F R} f [p1 p2] : rename.
 
 Section MaxRoots.
 
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 854335d..4008f1a 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -3727,23 +3727,23 @@ End TermDef.
 
 Bind Scope term_scope with term.
 Bind Scope term_scope with formula.
-Arguments Add {_} _%T _%T.
-Arguments Opp {_} _%T.
-Arguments NatMul {_} _%T _%N.
-Arguments Mul {_} _%T _%T.
-Arguments Inv {_} _%T.
-Arguments Exp {_} _%T _%N.
-Arguments Equal {_} _%T _%T.
-Arguments Unit {_} _%T.
-Arguments And {_} _%T _%T.
-Arguments Or {_} _%T _%T.
-Arguments Implies {_} _%T _%T.
-Arguments Not {_} _%T.
-Arguments Exists {_} _%N _%T.
-Arguments Forall {_} _%N _%T.
-
-Arguments Bool {R}.
-Arguments Const {R}.
+Arguments Add {R} t1%T t2%T.
+Arguments Opp {R} t1%T.
+Arguments NatMul {R} t1%T n%N.
+Arguments Mul {R} t1%T t2%T.
+Arguments Inv {R} t1%T.
+Arguments Exp {R} t1%T n%N.
+Arguments Equal {R} t1%T t2%T.
+Arguments Unit {R} t1%T.
+Arguments And {R} f1%T f2%T.
+Arguments Or {R} f1%T f2%T.
+Arguments Implies {R} f1%T f2%T.
+Arguments Not {R} f1%T.
+Arguments Exists {R} i%N f1%T.
+Arguments Forall {R} i%N f1%T.
+
+Arguments Bool {R} b.
+Arguments Const {R} x.
 
 Notation True := (Bool true).
 Notation False := (Bool false).
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index d0214dd..614fbc2 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -369,7 +369,7 @@ Canonical int_countIdomainType := [countIdomainType of int].
 Definition absz m := match m with Posz p => p | Negz n => n.+1 end.
 Notation "m - n" :=
   (@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope.
-Arguments absz _%distn_scope.
+Arguments absz m%distn_scope.
 Local Notation "`| m |" := (absz m) : nat_scope.
 
 Module intOrdered.
@@ -1607,7 +1607,7 @@ Module Export IntDist.
 
 Notation "m - n" :=
   (@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope.
-Arguments absz _%distn_scope.
+Arguments absz m%distn_scope.
 Notation "`| m |" := (absz m) : nat_scope.
 Coercion Posz : nat >-> int.
 
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index aef9a9f..542f8ad 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -245,7 +245,7 @@ Definition f2mx (f : 'Hom(aT, rT)) := let: Hom A := f in A.
 Canonical hom_subType := [newType for f2mx].
 End Hom.
 
-Arguments mx2vs _ _ _%N _%MS.
+Arguments mx2vs {K vT m%N} A%MS.
 Prenex Implicits v2r r2v v2rK r2vK b2mx vs2mx vs2mxK f2mx.
 
 End InternalTheory.