Merge pull request #253 from anton-trunov/arguments

Document parameter names whenever possible

35 files changed, 241 insertions, 250 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 c432f73..6df490d 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -3741,23 +3741,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.
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.
diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index 8a65f2b..ad2388a 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -260,7 +260,7 @@ Qed.
 Prenex Implicits alg_integral.
 
 Import DefaultKeying GRing.DefaultPred.
-Arguments map_poly_inj {F R} f [x1 x2].
+Arguments map_poly_inj {F R} f [p1 p2].
 
 Theorem Fundamental_Theorem_of_Algebraics :
   {L : closedFieldType &
diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v
index ca738ef..009c1ae 100644
--- a/mathcomp/field/closed_field.v
+++ b/mathcomp/field/closed_field.v
@@ -54,18 +54,18 @@ Proof. by split=> /andP[]. Qed.
 
 Notation cps T := ((T -> fF) -> fF).
 Definition ret T1 : T1 -> cps T1 := fun x k => k x.
-Arguments ret T1 x k /.
+Arguments ret {T1} x k /.
 
 Definition bind T1 T2 (x : cps T1) (f : T1 -> cps T2) : cps T2 :=
   fun k => x (fun x => f x k).
-Arguments bind T1 T2 x f k /.
+Arguments bind {T1 T2} x f k /.
 Notation "''let' x <- y ; z" :=
   (bind y (fun x => z)) (at level 99, x at level 0, y at level 0,
     format "'[hv' ''let'  x  <-  y ;  '/' z ']'").
 
 Definition cpsif T (c : fF) (t : T) (e : T) : cps T :=
   fun k => GRing.If c (k t) (k e).
-Arguments cpsif T c t e k /.
+Arguments cpsif {T} c t e k /.
 Notation "''if' c1 'then' c2 'else' c3" := (cpsif c1%T c2%T c3%T)
   (at level 200, right associativity, format
 "'[hv   ' ''if'  c1  '/' '[' 'then'  c2  ']' '/' '[' 'else'  c3 ']' ']'").
diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v
index 0410e55..7e86d3c 100644
--- a/mathcomp/field/falgebra.v
+++ b/mathcomp/field/falgebra.v
@@ -620,8 +620,8 @@ End FalgebraTheory.
 Delimit Scope aspace_scope with AS.
 Bind Scope aspace_scope with aspace.
 Bind Scope aspace_scope with aspace_of.
-Arguments asval _ _ _%AS.
-Arguments clone_aspace _ _ _%VS _%AS _ _.
+Arguments asval {K aT} a%AS.
+Arguments clone_aspace [K aT U%VS A%AS algU] _.
 
 Notation "{ 'aspace' T }" := (aspace_of (Phant T)) : type_scope.
 Notation "A * B" := (prodv A B) : vspace_scope.
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.
 
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index 1165a33..a68bc9f 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -493,7 +493,7 @@ Qed.
 End PreGroupIdentities.
 
 Hint Resolve commute1.
-Arguments invg_inj {T}.
+Arguments invg_inj {T} [x1 x2].
 Prenex Implicits commute invgK.
 
 Section GroupIdentities.
@@ -643,7 +643,7 @@ Definition gnorm := (gsimp, (mulgK, mulgKV, (mulgA, invMg))).
 
 Arguments mulgI [T].
 Arguments mulIg [T].
-Arguments conjg_inj [T].
+Arguments conjg_inj {T} x [x1 x2].
 Arguments commgP {T x y}.
 Arguments conjg_fixP {T x y}.
 
diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v
index 322fc4e..97b2eba 100644
--- a/mathcomp/fingroup/quotient.v
+++ b/mathcomp/fingroup/quotient.v
@@ -750,8 +750,8 @@ Qed.
 
 End EqIso.
 
-Arguments qisom_inj [gT G H].
-Arguments morphim_qisom_inj [gT G H].
+Arguments qisom_inj {gT G H} eqGH [x1 x2].
+Arguments morphim_qisom_inj {gT G H} eqGH [x1 x2].
 
 Section FirstIsomorphism.
 
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.
 
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 4487ab4..7473ed7 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -460,7 +460,7 @@ Notation "x |-> y" := (FunDelta x y)
    format "'[hv' x '/ '  |->  y ']'") : fun_delta_scope.
 
 Delimit Scope fun_delta_scope with FUN_DELTA.
-Arguments app_fdelta _ _%type _%FUN_DELTA _ _.
+Arguments app_fdelta {aT rT%type} df%FUN_DELTA f z.
 
 Notation "[ 'fun' z : T => F 'with' d1 , .. , dn ]" :=
   (SimplFunDelta (fun z : T =>
@@ -603,7 +603,7 @@ Arguments vrefl_rect {T P}.
 Arguments clone_subType [T P] U v [sT] _ [c Urec cK].
 Arguments insub {T P sT}.
 Arguments insubT [T] P [sT x].
-Arguments val_inj {T P sT}.
+Arguments val_inj {T P sT} [x1 x2].
 Prenex Implicits val insubd.
 
 Local Notation inlined_sub_rect :=
@@ -779,7 +779,7 @@ Proof. by case/andP. Qed.
 
 End ProdEqType.
 
-Arguments pair_eq {T1 T2} _ _ /.
+Arguments pair_eq {T1 T2} u v /.
 Arguments pair_eqP {T1 T2}.
 
 Definition predX T1 T2 (p1 : pred T1) (p2 : pred T2) :=
@@ -805,7 +805,7 @@ Canonical option_eqType := Eval hnf in EqType (option T) option_eqMixin.
 
 End OptionEqType.
 
-Arguments opt_eq {T} !_ !_.
+Arguments opt_eq {T} !u !v.
 
 Section TaggedAs.
 
@@ -851,7 +851,7 @@ Proof. by rewrite -tag_eqE /tag_eq eqxx tagged_asE. Qed.
 
 End TagEqType.
 
-Arguments tag_eq {I T_} !_ !_.
+Arguments tag_eq {I T_} !u !v.
 Arguments tag_eqP {I T_ x y}.
 
 Section SumEqType.
@@ -875,5 +875,5 @@ Lemma sum_eqE : sum_eq = eq_op. Proof. by []. Qed.
 
 End SumEqType.
 
-Arguments sum_eq {T1 T2} !_ !_.
+Arguments sum_eq {T1 T2} !u !v.
 Arguments sum_eqP {T1 T2 x y}.
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 3fd10fa..4ad02c6 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -130,7 +130,7 @@ Delimit Scope set_scope with SET.
 Bind Scope set_scope with set_type.
 Bind Scope set_scope with set_of.
 Open Scope set_scope.
-Arguments finfun_of_set _ _%SET.
+Arguments finfun_of_set {T} A%SET.
 
 Notation "{ 'set' T }" := (set_of (Phant T))
   (at level 0, format "{ 'set'  T }") : type_scope.
@@ -955,7 +955,7 @@ Proof. by rewrite setDE disjoints_subset => /properI/andP[-> /proper_sub]. Qed.
 End setOps.
 
 Arguments set1P {T x a}.
-Arguments set1_inj {T}.
+Arguments set1_inj {T} [x1 x2].
 Arguments set2P {T x a b}.
 Arguments setIdP {T x pA pB}.
 Arguments setIP {T x A B}.
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 4b2952f..d4f564f 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -1760,7 +1760,7 @@ Qed.
 
 End EnumRank.
 
-Arguments enum_val_inj {T A} [x1 x2].
+Arguments enum_val_inj {T A} [i1 i2] : rename.
 Arguments enum_rank_inj {T} [x1 x2].
 Prenex Implicits enum_val enum_rank.
 
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index b24da11..b8388f0 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -174,7 +174,7 @@ Qed.
 Canonical nat_eqMixin := EqMixin eqnP.
 Canonical nat_eqType := Eval hnf in EqType nat nat_eqMixin.
 
-Arguments eqn !_ !_.
+Arguments eqn !m !n.
 Arguments eqnP {x y}.
 
 Lemma eqnE : eqn = eq_op. Proof. by []. Qed.
@@ -1454,7 +1454,7 @@ Qed.
 Canonical bin_nat_eqMixin := EqMixin eq_binP.
 Canonical bin_nat_eqType := Eval hnf in EqType N bin_nat_eqMixin.
 
-Arguments N.eqb !_ !_.
+Arguments N.eqb !n !m.
 
 Section NumberInterpretation.