Merge pull request #185 from jashug/deprecate-arguments-scope

Change deprecated Arguments Scope to Arguments

40 files changed, 293 insertions, 334 deletions

diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index b54e586..ec9fcc5 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -2660,7 +2660,7 @@ Coercion GLval ph (u : GLtype ph) : 'M[R]_n.-1.+1 :=
 End FinUnitMatrix.
 
 Bind Scope group_scope with GLtype.
-Arguments Scope GLval [nat_scope _ _ group_scope].
+Arguments GLval _%N _ _ _%g.
 Prenex Implicits GLval.
 
 Notation "{ ''GL_' n [ R ] }" := (GLtype n (Phant R))
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index 9cf3f6e..d77bfb1 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -216,9 +216,9 @@ Definition pinvmx : 'M_(n, m) :=
 
 End Defs.
 
-Arguments Scope mxrank [nat_scope nat_scope matrix_set_scope].
+Arguments mxrank _%N _%N _%MS.
 Local Notation "\rank A" := (mxrank A) : nat_scope.
-Arguments Scope complmx [nat_scope nat_scope matrix_set_scope].
+Arguments complmx _%N _%N _%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,8 +227,7 @@ Fact submx_key : unit. Proof. by []. Qed.
 Definition submx := locked_with submx_key submx_def.
 Canonical submx_unlockable := [unlockable fun submx].
 
-Arguments Scope submx
-  [nat_scope nat_scope nat_scope matrix_set_scope matrix_set_scope].
+Arguments submx _%N _%N _%N _%MS _%MS.
 Prenex Implicits submx.
 Local Notation "A <= B" := (submx A B) : matrix_set_scope.
 Local Notation "A <= B <= C" := ((A <= B) && (B <= C))%MS : matrix_set_scope.
@@ -236,8 +235,7 @@ 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 Scope ltmx
-  [nat_scope nat_scope nat_scope matrix_set_scope matrix_set_scope].
+Arguments ltmx _%N _%N _%N _%MS _%MS.
 Prenex Implicits ltmx.
 Local Notation "A < B" := (ltmx A B) : matrix_set_scope.
 
@@ -245,8 +243,7 @@ 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 Scope eqmx
-  [nat_scope nat_scope nat_scope matrix_set_scope matrix_set_scope].
+Arguments eqmx _%N _%N _%N _%MS _%MS.
 Local Notation "A :=: B" := (eqmx A B) : matrix_set_scope.
 
 Section LtmxIdentities.
@@ -301,8 +298,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 Scope addsmx
-  [nat_scope nat_scope nat_scope matrix_set_scope matrix_set_scope].
+Arguments addsmx _%N _%N _%N _%MS _%MS.
 Prenex Implicits addsmx.
 Local Notation "A + B" := (addsmx A B) : matrix_set_scope.
 Local Notation "\sum_ ( i | P ) B" := (\big[addsmx/0]_(i | P) B%MS)
@@ -337,8 +333,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 Scope capmx
-  [nat_scope nat_scope nat_scope matrix_set_scope matrix_set_scope].
+Arguments capmx _%N _%N _%N _%MS _%MS.
 Prenex Implicits capmx.
 Local Notation "A :&: B" := (capmx A B) : matrix_set_scope.
 Local Notation "\bigcap_ ( i | P ) B" := (\big[capmx/1%:M]_(i | P) B)
@@ -349,8 +344,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 Scope diffmx
-  [nat_scope nat_scope nat_scope matrix_set_scope matrix_set_scope].
+Arguments diffmx _%N _%N _%N _%MS _%MS.
 Prenex Implicits diffmx.
 Local Notation "A :\: B" := (diffmx A B) : matrix_set_scope.
 
@@ -1735,7 +1729,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 Scope mxsum_spec [nat_scope nat_scope matrix_set_scope nat_scope].
+Arguments mxsum_spec _%N _%N _%MS _%N.
 
 Structure mxsum_expr m n := Mxsum {
   mxsum_val :> wrapped 'M_(m, n);
@@ -2005,21 +1999,15 @@ Arguments mxdirect_sumsE [F I P n S_].
 Arguments eigenspaceP [F n g a m W].
 Arguments eigenvalueP [F n g a].
 
-Arguments Scope mxrank [_ nat_scope nat_scope matrix_set_scope].
-Arguments Scope complmx [_ nat_scope nat_scope matrix_set_scope].
-Arguments Scope row_full [_ nat_scope nat_scope matrix_set_scope].
-Arguments Scope submx
-  [_ nat_scope nat_scope nat_scope matrix_set_scope matrix_set_scope].
-Arguments Scope ltmx
-  [_ nat_scope nat_scope nat_scope matrix_set_scope matrix_set_scope].
-Arguments Scope eqmx
-  [_ nat_scope nat_scope nat_scope matrix_set_scope matrix_set_scope].
-Arguments Scope addsmx
-  [_ nat_scope nat_scope nat_scope matrix_set_scope matrix_set_scope].
-Arguments Scope capmx
-  [_ nat_scope nat_scope nat_scope matrix_set_scope matrix_set_scope].
-Arguments Scope diffmx
-  [_ nat_scope nat_scope nat_scope matrix_set_scope matrix_set_scope].
+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 mxrank genmx complmx submx ltmx addsmx capmx.
 Notation "\rank A" := (mxrank A) : nat_scope.
 Notation "<< A >>" := (genmx A) : matrix_set_scope.
@@ -2295,8 +2283,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 Scope mulsmx
-  [nat_scope nat_scope nat_scope matrix_set_scope matrix_set_scope].
+Arguments mulsmx _%N _%N _%N _%MS _%MS.
 
 Local Notation "R1 * R2" := (mulsmx R1 R2) : matrix_set_scope.
 
@@ -2606,24 +2593,15 @@ Qed.
 
 End MatrixAlgebra.
 
-Arguments Scope mulsmx
-  [_ nat_scope nat_scope nat_scope matrix_set_scope matrix_set_scope].
-Arguments Scope left_mx_ideal
-  [_ nat_scope nat_scope nat_scope matrix_set_scope matrix_set_scope].
-Arguments Scope right_mx_ideal
-  [_ nat_scope nat_scope nat_scope matrix_set_scope matrix_set_scope].
-Arguments Scope mx_ideal
-  [_ nat_scope nat_scope nat_scope matrix_set_scope matrix_set_scope].
-Arguments Scope mxring_id
-  [_ nat_scope nat_scope ring_scope matrix_set_scope].
-Arguments Scope has_mxring_id
-  [_ nat_scope nat_scope ring_scope matrix_set_scope].
-Arguments Scope mxring
-  [_ nat_scope nat_scope matrix_set_scope].
-Arguments Scope cent_mx
-  [_ nat_scope nat_scope matrix_set_scope].
-Arguments Scope center_mx
-  [_ nat_scope nat_scope matrix_set_scope].
+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.
 
 Prenex Implicits mulsmx.
 
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index 409930c..f34ca2d 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 Scope polyseq [_ ring_scope].
-Arguments Scope poly_inj [_ ring_scope ring_scope _].
-Arguments Scope coefp_head [_ _ nat_scope ring_scope _].
+Arguments polyseq _ _%R.
+Arguments poly_inj _ _%R _%R _.
+Arguments coefp_head _ _ _%N _%R.
 Notation "{ 'poly' T }" := (poly_of (Phant T)).
 Notation coefp i := (coefp_head tt i).
 
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 1725e5e..c0b3041 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -3724,21 +3724,20 @@ End TermDef.
 
 Bind Scope term_scope with term.
 Bind Scope term_scope with formula.
-Arguments Scope Add [_ term_scope term_scope].
-Arguments Scope Opp [_ term_scope].
-Arguments Scope NatMul [_ term_scope nat_scope].
-Arguments Scope Mul [_ term_scope term_scope].
-Arguments Scope Mul [_ term_scope term_scope].
-Arguments Scope Inv [_ term_scope].
-Arguments Scope Exp [_ term_scope nat_scope].
-Arguments Scope Equal [_ term_scope term_scope].
-Arguments Scope Unit [_ term_scope].
-Arguments Scope And [_ term_scope term_scope].
-Arguments Scope Or [_ term_scope term_scope].
-Arguments Scope Implies [_ term_scope term_scope].
-Arguments Scope Not [_ term_scope].
-Arguments Scope Exists [_ nat_scope term_scope].
-Arguments Scope Forall [_ nat_scope term_scope].
+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].
 Prenex Implicits Const Add Opp NatMul Mul Exp Bool Unit And Or Implies Not.
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index 752be45..cbfd593 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -362,7 +362,7 @@ Canonical int_iDomain :=
 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 Scope absz [distn_scope].
+Arguments absz _%distn_scope.
 Local Notation "`| m |" := (absz m) : nat_scope.
 
 Module intOrdered.
@@ -1600,7 +1600,7 @@ Module Export IntDist.
 
 Notation "m - n" :=
   (@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope.
-Arguments Scope absz [distn_scope].
+Arguments absz _%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 73354bf..a2346a2 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 Scope mx2vs [_ _ nat_scope matrix_set_scope].
+Arguments mx2vs _ _ _%N _%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 ad0fa32..e522924 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 Scope pred_Nirr [_ group_scope].
+Arguments pred_Nirr _ _%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 Scope socle_of_Iirr [_ ring_scope].
+Arguments socle_of_Iirr _ _%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 Scope irr [_ group_scope].
+Arguments irr _ _%g.
 
 Notation "''chi_' i" :=  (tnth (irr _) i%R)
   (at level 8, i at level 2, format "''chi_' i") : ring_scope.
@@ -816,7 +816,7 @@ Qed.
 
 End IrrClass.
 
-Arguments Scope cfReg [_ group_scope].
+Arguments cfReg _ _%g.
 Prenex Implicits cfIirr.
 Arguments irr_inj {gT G} [x1 x2].
 
@@ -1334,7 +1334,7 @@ Qed.
 
 End OrthogonalityRelations.
 
-Arguments Scope character_table [_ group_scope].
+Arguments character_table _ _%g.
 
 Section InnerProduct.
 
@@ -1565,7 +1565,7 @@ Qed.
 
 End IrrConstt.
 
-Arguments Scope irr_constt [_ group_scope cfun_scope].
+Arguments irr_constt _ _%g _%CF.
 
 Section Kernel.
 
@@ -1733,7 +1733,7 @@ Qed.
 
 End Restrict.
 
-Arguments Scope Res_Iirr [_ group_scope group_scope ring_scope].
+Arguments Res_Iirr _ _%g _%g _%R.
 
 Section MoreConstt.
 
@@ -2993,4 +2993,4 @@ Proof. by move/cfker_Ind->; rewrite ?irr_neq0 ?irr_char. Qed.
 
 End Induced.
 
-Arguments Scope Ind_Iirr [_ group_scope group_scope ring_scope].
\ No newline at end of file
+Arguments Ind_Iirr _ _%g _%g _%R.
\ No newline at end of file
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 3afaa82..7a0e538 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -392,14 +392,14 @@ End Defs.
 
 Bind Scope cfun_scope with classfun.
 
-Arguments Scope classfun [_ group_scope].
-Arguments Scope classfun_on [_ group_scope group_scope].
-Arguments Scope cfun_indicator [_ group_scope].
-Arguments Scope cfAut [_ group_scope _ cfun_scope].
-Arguments Scope cfReal [_ group_scope cfun_scope].
-Arguments Scope cfdot [_ group_scope cfun_scope cfun_scope].
-Arguments Scope cfdotr_head [_ group_scope _ cfun_scope cfun_scope].
-Arguments Scope cfdotr_head [_ group_scope _ cfun_scope].
+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.
 
 Notation "''CF' ( G )" := (classfun G) : type_scope.
 Notation "''CF' ( G )" := (@fullv _ (cfun_vectType G)) : vspace_scope.
@@ -452,12 +452,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 Scope cfker [_ group_scope cfun_scope].
-Arguments Scope cfaithful [_ group_scope cfun_scope].
-Arguments Scope orthogonal [_ group_scope cfun_scope cfun_scope].
-Arguments Scope pairwise_orthogonal [_ group_scope cfun_scope].
-Arguments Scope orthonormal [_ group_scope cfun_scope].
-Arguments Scope isometry [_ _ group_scope group_scope cfun_scope].
+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.
 
 Notation "{ 'in' CFD , 'isometry' tau , 'to' CFR }" :=
     (isometry_from_to (mem CFD) tau (mem CFR))
@@ -756,7 +756,7 @@ Proof. by []. Qed.
 
 End ClassFun.
 
-Arguments Scope classfun_on [_ group_scope group_scope].
+Arguments classfun_on _ _%g _%g.
 Notation "''CF' ( G , A )" := (classfun_on G A) : ring_scope.
 
 Arguments cfun_onP [gT G A phi].
@@ -1394,7 +1394,7 @@ Canonical cfRes_lrmorphism := [lrmorphism of cfRes].
 
 End Restrict.
 
-Arguments Scope cfRes [_ group_scope group_scope cfun_scope].
+Arguments cfRes _ _%g _%g _%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.
@@ -1727,8 +1727,8 @@ Proof. by move=> nsBG kerH; rewrite -cfMod_eq1 // cfQuoK. Qed.
 
 End Coset.
 
-Arguments Scope cfQuo [_ Group_scope group_scope cfun_scope].
-Arguments Scope cfMod [_ Group_scope group_scope cfun_scope].
+Arguments cfQuo _ _%G _%g _%CF.
+Arguments cfMod _ _%G _%g _%CF.
 Prenex Implicits cfMod.
 Notation "phi / H" := (cfQuo H phi) : cfun_scope.
 Notation "phi %% H" := (@cfMod _ _ H phi) : cfun_scope.
@@ -2327,7 +2327,7 @@ Qed.
 
 End Induced.
 
-Arguments Scope cfInd [_ group_scope group_scope cfun_scope].
+Arguments cfInd _ _%g _%g _%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.
diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v
index 7d4a84c..ffa9696 100644
--- a/mathcomp/character/inertia.v
+++ b/mathcomp/character/inertia.v
@@ -567,8 +567,8 @@ Qed.
 
 End Inertia.
 
-Arguments Scope inertia [_ group_scope cfun_scope].
-Arguments Scope cfclass [_ group_scope cfun_scope group_scope].
+Arguments inertia _ _%g _%CF.
+Arguments cfclass _ _%g _%CF _%g.
 Arguments conjg_Iirr_inj [gT H] y [x1 x2].
 
 Notation "''I[' phi ] " := (inertia phi) : group_scope.
diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v
index 16e3b51..f0553f2 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 Scope gring_irr_mode [_ Group_scope ring_scope group_scope].
+Arguments gring_irr_mode _ _%G _%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 92fdb0e..b121f4c 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 Scope rowg_mx [_ _ group_scope].
+Arguments rowg_mx _ _ _%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 Scope abelem_dim' [_ group_scope].
+Arguments abelem_dim' _ _%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 fbd4bc3..4558b3d 100644
--- a/mathcomp/character/mxrepresentation.v
+++ b/mathcomp/character/mxrepresentation.v
@@ -291,7 +291,7 @@ Structure mx_representation G n :=
   MxRepresentation { repr_mx :> gT -> 'M_n; _ : mx_repr G repr_mx }.
 
 Variables (G : {group gT}) (n : nat) (rG : mx_representation G n).
-Arguments Scope rG [group_scope].
+Arguments rG _%group_scope : extra scopes.
 
 Lemma repr_mx1 : rG 1 = 1%:M.
 Proof. by case: rG => r []. Qed.
@@ -814,10 +814,10 @@ End Regular.
 
 End RingRepr.
 
-Arguments Scope mx_representation [_ _ group_scope nat_scope].
-Arguments Scope mx_repr [_ _ group_scope nat_scope _].
-Arguments Scope group_ring [_ _ group_scope].
-Arguments Scope regular_repr [_ _ group_scope].
+Arguments mx_representation _ _ _%g _%N.
+Arguments mx_repr _ _ _%g _%N _.
+Arguments group_ring _ _ _%g.
+Arguments regular_repr _ _ _%g.
 
 Arguments centgmxP [R gT G n rG f].
 Arguments rkerP [R gT G n rG x].
@@ -891,7 +891,7 @@ Section OneRepresentation.
 Variable gT : finGroupType.
 
 Variables (G : {group gT}) (n : nat) (rG : mx_representation F G n).
-Arguments Scope rG [group_scope].
+Arguments rG _%group_scope : extra scopes.
 
 Local Notation E_G := (enveloping_algebra_mx rG).
 
@@ -4654,10 +4654,10 @@ End LinearIrr.
 
 End FieldRepr.
 
-Arguments Scope rfix_mx [_ _ group_scope nat_scope _ group_scope].
-Arguments Scope gset_mx [_ _ group_scope group_scope].
-Arguments Scope classg_base [_ _ group_scope group_scope].
-Arguments Scope irrType [_ _ group_scope group_scope].
+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 mxmoduleP [F gT G n rG m U].
 Arguments envelop_mxP [F gT G n rG A].
@@ -4681,9 +4681,9 @@ Notation "'Cl" := (Clifford_action _) : action_scope.
 
 Bind Scope irrType_scope with socle_sort.
 Notation "[ 1 sG ]" := (principal_comp sG) : irrType_scope.
-Arguments Scope irr_degree [_ _ Group_scope _ irrType_scope].
-Arguments Scope irr_repr [_ _ Group_scope _ irrType_scope group_scope].
-Arguments Scope irr_mode [_ _ Group_scope _ irrType_scope group_scope].
+Arguments irr_degree _ _ _%G _ _%irr.
+Arguments irr_repr _ _ _%G _ _%irr _%g : extra scopes.
+Arguments irr_mode _ _ _%G _ _%irr _%g : extra scopes.
 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/falgebra.v b/mathcomp/field/falgebra.v
index e0ae1b1..ada61bc 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 Scope asval [_ _ aspace_scope].
-Arguments Scope clone_aspace [_ _ vspace_scope aspace_scope _ _].
+Arguments asval _ _ _%AS.
+Arguments clone_aspace _ _ _%VS _%AS _ _.
 
 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 6478c81..5c5dcdc 100644
--- a/mathcomp/fingroup/action.v
+++ b/mathcomp/fingroup/action.v
@@ -148,11 +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 Scope act_morph [_ group_scope _ _ group_scope].
-Arguments Scope is_action [_ group_scope _ _].
-Arguments Scope act
-  [_ group_scope type_scope action_scope group_scope group_scope].
-Arguments Scope clone_action [_ group_scope type_scope action_scope _].
+Arguments act_morph _ _%g _ _ _%g : extra scopes.
+Arguments is_action _ _%g _ _.
+Arguments act _ _%g _%type _%act _%g _%g.
+Arguments clone_action _ _%g _%type _%act _.
 
 Notation "{ 'action' aT &-> T }" := (action [set: aT] T)
   (at level 0, format "{ 'action'  aT  &->  T }") : type_scope.
@@ -211,16 +210,15 @@ Definition faithful A S to := A :&: astab S to \subset [1].
 
 End ActionDefs.
 
-Arguments Scope setact [_ group_scope _ action_scope group_scope group_scope].
-Arguments Scope orbit [_ group_scope _ action_scope group_scope group_scope].
-Arguments Scope amove
-  [_ group_scope _ action_scope group_scope group_scope group_scope].
-Arguments Scope afix [_ group_scope _ action_scope group_scope].
-Arguments Scope astab [_ group_scope _ group_scope action_scope].
-Arguments Scope astabs [_ group_scope _ group_scope action_scope].
-Arguments Scope acts_on [_ group_scope _ group_scope group_scope action_scope].
-Arguments Scope atrans [_ group_scope _ group_scope group_scope action_scope].
-Arguments Scope faithful [_ group_scope _ group_scope group_scope action_scope].
+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.
 
 Notation "to ^*" := (setact to) (at level 2, format "to ^*") : fun_scope.
 
@@ -877,8 +875,7 @@ Qed.
 
 End PartialAction.
 
-Arguments Scope orbit_transversal
-  [_ group_scope _ action_scope group_scope group_scope].
+Arguments orbit_transversal _ _%g _ _%act _%g _%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].
@@ -1748,7 +1745,7 @@ Qed.
 
 End AutIn.
 
-Arguments Scope Aut_in [_ group_scope group_scope].
+Arguments Aut_in _ _%g _%g.
 
 Section InjmAutIn.
 
@@ -1825,9 +1822,9 @@ End GroupAction.
 Delimit Scope groupAction_scope with gact.
 Bind Scope groupAction_scope with groupAction.
 
-Arguments Scope is_groupAction [_ _ group_scope group_scope action_scope].
-Arguments Scope groupAction [_ _ group_scope group_scope].
-Arguments Scope gact [_ _ group_scope group_scope groupAction_scope].
+Arguments is_groupAction _ _ _%g _%g _%act.
+Arguments groupAction _ _ _%g _%g.
+Arguments gact _ _ _%g _%g _%gact.
 
 Notation "[ 'groupAction' 'of' to ]" :=
      (clone_groupAction (@GroupAction _ _ _ _ to))
@@ -1854,12 +1851,9 @@ Definition acts_irreducibly A S to :=
 
 End GroupActionDefs.
 
-Arguments Scope gacent
-  [_ _ group_scope group_scope groupAction_scope group_scope].
-Arguments Scope acts_on_group
-  [_ _ group_scope group_scope group_scope group_scope groupAction_scope].
-Arguments Scope acts_irreducibly
-  [_ _ group_scope group_scope group_scope group_scope groupAction_scope].
+Arguments gacent _ _ _%g _%g _%gact _%g.
+Arguments acts_on_group _ _ _%g _%g _%g _%g _%gact.
+Arguments acts_irreducibly _ _ _%g _%g _%g _%g _%gact.
 
 Notation "''C_' ( | to ) ( A )" := (gacent to A)
   (at level 8, format "''C_' ( | to ) ( A )") : group_scope.
@@ -2715,8 +2709,8 @@ Canonical aut_groupAction := GroupAction autact_is_groupAction.
 
 End AutAct.
 
-Arguments Scope aut_action [_ group_scope].
-Arguments Scope aut_groupAction [_ group_scope].
+Arguments aut_action _ _%g.
+Arguments aut_groupAction _ _%g.
 Notation "[ 'Aut' G ]" := (aut_action G) : action_scope.
 Notation "[ 'Aut' G ]" := (aut_groupAction G) : groupAction_scope.
 
diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v
index e727aba..b1c9d94 100644
--- a/mathcomp/fingroup/automorphism.v
+++ b/mathcomp/fingroup/automorphism.v
@@ -115,7 +115,7 @@ Qed.
 
 End Automorphism.
 
-Arguments Scope Aut [_ group_scope].
+Arguments Aut _ _%g.
 Notation "[ 'Aut' G ]" := (Aut_group G)
   (at level 0, format "[ 'Aut'  G ]") : Group_scope.
 Notation "[ 'Aut' G ]" := (Aut G)
@@ -340,7 +340,7 @@ Proof. by apply/subsetP=> _ /imsetP[x _ ->]; apply: Aut_aut. Qed.
 
 End ConjugationMorphism.
 
-Arguments Scope conjgm [_ group_scope].
+Arguments conjgm _ _%g.
 Prenex Implicits conjgm conj_aut.
 
 Reserved Notation "G \char H" (at level 70).
@@ -447,7 +447,7 @@ Qed.
 
 End Characteristicity.
 
-Arguments Scope characteristic [_ group_scope group_scope].
+Arguments characteristic _ _%g _%g.
 Notation "H \char G" := (characteristic H G) : group_scope.
 Hint Resolve char_refl.
 
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index 5afc3c7..b43036b 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -791,25 +791,24 @@ Definition centralised A := forall x, centralises x A.
 
 End GroupSetMulDef.
 
-Arguments Scope lcoset [_ group_scope group_scope].
-Arguments Scope rcoset [_ group_scope group_scope].
-Arguments Scope rcosets [_ group_scope group_scope].
-Arguments Scope lcosets [_ group_scope group_scope].
-Arguments Scope indexg [_ group_scope group_scope].
-Arguments Scope conjugate [_ group_scope group_scope].
-Arguments Scope conjugates [_ group_scope group_scope].
-Arguments Scope class [_ group_scope group_scope].
-Arguments Scope classes [_ group_scope].
-Arguments Scope class_support [_ group_scope group_scope].
-Arguments Scope commg_set [_ group_scope group_scope].
-Arguments Scope normaliser [_ group_scope].
-Arguments Scope centraliser [_ group_scope].
-Arguments Scope abelian [_ group_scope].
-Arguments Scope normal [_ group_scope group_scope].
-Arguments Scope centralised [_ group_scope].
-Arguments Scope normalised [_ group_scope].
-Arguments Scope centralises [_ group_scope group_scope].
-Arguments Scope centralised [_ group_scope].
+Arguments lcoset _ _%g _%g.
+Arguments rcoset _ _%g _%g.
+Arguments rcosets _ _%g _%g.
+Arguments lcosets _ _%g _%g.
+Arguments indexg _ _%g _%g.
+Arguments conjugate _ _%g _%g.
+Arguments conjugates _ _%g _%g.
+Arguments class _ _%g _%g.
+Arguments classes _ _%g.
+Arguments class_support _ _%g _%g.
+Arguments commg_set _ _%g _%g.
+Arguments normaliser _ _%g.
+Arguments centraliser _ _%g.
+Arguments abelian _ _%g.
+Arguments normal _ _%g _%g.
+Arguments normalised _ _%g.
+Arguments centralises _ _%g _%g.
+Arguments centralised _ _%g.
 
 Notation "[ 1 gT ]" := (1 : {set gT}) : group_scope.
 Notation "[ 1 ]" := [1 FinGroup.sort _] : group_scope.
@@ -1312,9 +1311,9 @@ Arguments group_setP [gT A].
 Prenex Implicits group_set mulsgP set1gP.
 Prenex Implicits lcosetP lcosetsP rcosetP rcosetsP group_setP.
 
-Arguments Scope commutator [_ group_scope group_scope].
-Arguments Scope joing [_ group_scope group_scope].
-Arguments Scope generated [_ group_scope].
+Arguments commutator _ _%g _%g.
+Arguments joing _ _%g _%g.
+Arguments generated _ _%g.
 
 Notation "{ 'group' gT }" := (group_of (Phant gT))
   (at level 0, format "{ 'group'  gT }") : type_scope.
@@ -1913,9 +1912,9 @@ End GroupInter.
 
 Hint Resolve order_gt0.
 
-Arguments Scope generated_group [_ group_scope].
-Arguments Scope joing_group [_ group_scope group_scope].
-Arguments Scope subgroups [_ group_scope].
+Arguments generated_group _ _%g.
+Arguments joing_group _ _%g _%g.
+Arguments subgroups _ _%g.
 
 Notation "G :&: H" := (setI_group G H) : Group_scope.
 Notation "<< A >>"  := (generated_group A) : Group_scope.
@@ -2997,8 +2996,8 @@ Arguments commG1P [gT A B].
 
 Prenex Implicits normP normsP cent1P normalP centP centsP commG1P.
 
-Arguments Scope normaliser_group [_ group_scope].
-Arguments Scope centraliser_group [_ group_scope].
+Arguments normaliser_group _ _%g.
+Arguments centraliser_group _ _%g.
 
 Notation "''N' ( A )" := (normaliser_group A) : Group_scope.
 Notation "''C' ( A )" := (centraliser_group A) : Group_scope.
@@ -3017,7 +3016,7 @@ Section MinMaxGroup.
 
 Variable gT : finGroupType.
 Variable gP : pred {group gT}.
-Arguments Scope gP [Group_scope].
+Arguments gP _%G.
 
 Definition maxgroup := maxset (fun A => group_set A && gP <<A>>).
 Definition mingroup := minset (fun A => group_set A && gP <<A>>).
diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v
index dc16021..9498de7 100644
--- a/mathcomp/fingroup/gproduct.v
+++ b/mathcomp/fingroup/gproduct.v
@@ -89,16 +89,13 @@ Definition divgr A B x := x * (remgr A B x)^-1.
 
 End Defs.
 
-Arguments Scope partial_product [_ group_scope group_scope].
-Arguments Scope semidirect_product [_ group_scope group_scope].
-Arguments Scope central_product [_ group_scope group_scope].
-Arguments Scope complements_to_in [_ group_scope group_scope].
-Arguments Scope splits_over [_ group_scope group_scope].
-Arguments Scope remgr [_ group_scope group_scope group_scope].
-Arguments Scope divgr [_ group_scope group_scope group_scope].
-Arguments partial_product : clear implicits.
-Arguments semidirect_product : clear implicits.
-Arguments central_product : clear implicits.
+Arguments partial_product _ _%g _%g : clear implicits.
+Arguments semidirect_product _ _%g _%g : clear implicits.
+Arguments central_product _ _%g _%g : clear implicits.
+Arguments complements_to_in _ _%g _%g.
+Arguments splits_over _ _%g _%g.
+Arguments remgr _ _%g _%g _%g.
+Arguments divgr _ _%g _%g _%g.
 Arguments direct_product : clear implicits.
 Notation pprod := (partial_product _).
 Notation sdprod := (semidirect_product _).
diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v
index 315358b..32c01d3 100644
--- a/mathcomp/fingroup/morphism.v
+++ b/mathcomp/fingroup/morphism.v
@@ -144,8 +144,8 @@ Definition ker mph := morphpre mph 1.
 
 End MorphismOps1.
 
-Arguments Scope morphim [_ _ group_scope _ _ group_scope].
-Arguments Scope morphpre [_ _ group_scope _ _ group_scope].
+Arguments morphim _ _ _%g _ _ _%g.
+Arguments morphpre _ _ _%g _ _ _%g.
 
 Notation "''dom' f" := (dom (MorPhantom f))
   (at level 10, f at level 8, format "''dom'  f") : group_scope.
@@ -908,7 +908,7 @@ Proof. exact: morphim_idm. Qed.
 
 End IdentityMorphism.
 
-Arguments Scope idm [_ group_scope group_scope].
+Arguments idm _ _%g _%g.
 Prenex Implicits idm.
 
 Section RestrictedMorphism.
@@ -967,7 +967,7 @@ Proof. by move <-; exists f. Qed.
 
 End RestrictedMorphism.
 
-Arguments Scope restrm [_ _ group_scope group_scope _ group_scope].
+Arguments restrm _ _ _%g _%g _ _%g.
 Prenex Implicits restrm.
 Arguments restrmP [aT rT A D].
 Arguments domP [aT rT A D].
@@ -994,8 +994,7 @@ Proof. by apply/setIidPl/subsetP=> x _; rewrite !inE /=. Qed.
 
 End TrivMorphism.
 
-Arguments Scope trivm [_ _ group_scope group_scope].
-Arguments trivm {aT rT}.
+Arguments trivm {aT rT} _%g _%g.
 
 (* The composition of two morphisms is a Canonical morphism instance. *)
 Section MorphismComposition.
@@ -1325,10 +1324,10 @@ Proof. exact: restr_isom_to. Qed.
 
 End ReflectProp.
 
-Arguments Scope isom [_ _ group_scope group_scope _].
-Arguments Scope morphic [_ _ group_scope _].
-Arguments Scope misom [_ _ group_scope group_scope _].
-Arguments Scope isog [_ _ group_scope group_scope].
+Arguments isom _ _ _%g _%g _.
+Arguments morphic _ _ _%g _.
+Arguments misom _ _ _%g _%g _.
+Arguments isog _ _ _%g _%g.
 
 Arguments morphicP [aT rT A f].
 Arguments misomP [aT rT A B f].
@@ -1479,7 +1478,7 @@ Qed.
 
 End Homg.
 
-Arguments Scope homg [_ _ group_scope group_scope].
+Arguments homg _ _ _%g _%g.
 Notation "G \homg H" := (homg G H)
   (at level 70, no associativity) : group_scope.
 
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index bbf4363..ed5d25b 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -79,7 +79,7 @@ End PermDefSection.
 Notation "{ 'perm' T }" := (perm_of (Phant T))
   (at level 0, format "{ 'perm'  T }") : type_scope.
 
-Arguments Scope pval [_ group_scope].
+Arguments pval _ _%g.
 
 Bind Scope group_scope with perm_type.
 Bind Scope group_scope with perm_of.
diff --git a/mathcomp/fingroup/presentation.v b/mathcomp/fingroup/presentation.v
index ad712ee..7e3ad3c 100644
--- a/mathcomp/fingroup/presentation.v
+++ b/mathcomp/fingroup/presentation.v
@@ -134,17 +134,17 @@ Coercion Formula : formula >-> type.
 
 (* Declare (implicitly) the argument scope tags. *)
 Notation "1" := Idx : group_presentation.
-Arguments Scope Inv [group_presentation].
-Arguments Scope Exp [group_presentation nat_scope].
-Arguments Scope Mul [group_presentation group_presentation].
-Arguments Scope Conj [group_presentation group_presentation].
-Arguments Scope Comm [group_presentation group_presentation].
-Arguments Scope Eq1 [group_presentation].
-Arguments Scope Eq2 [group_presentation group_presentation].
-Arguments Scope Eq3 [group_presentation group_presentation group_presentation].
-Arguments Scope And [group_presentation group_presentation].
-Arguments Scope Formula [group_presentation].
-Arguments Scope Cast [group_presentation].
+Arguments Inv _%group_presentation.
+Arguments Exp _%group_presentation _%N.
+Arguments Mul _%group_presentation _%group_presentation.
+Arguments Conj _%group_presentation _%group_presentation.
+Arguments Comm _%group_presentation _%group_presentation.
+Arguments Eq1 _%group_presentation.
+Arguments Eq2 _%group_presentation _%group_presentation.
+Arguments Eq3 _%group_presentation _%group_presentation _%group_presentation.
+Arguments And _%group_presentation _%group_presentation.
+Arguments Formula _%group_presentation.
+Arguments Cast _%group_presentation.
 
 Infix "*" := Mul : group_presentation.
 Infix "^+" := Exp : group_presentation.
@@ -160,9 +160,9 @@ Notation "( r1 , r2 , .. , rn )" :=
 
 (* Declare (implicitly) the argument scope tags. *)
 Notation "x : p" := (fun x => Cast p) : nt_group_presentation.
-Arguments Scope Generator [nt_group_presentation].
-Arguments Scope hom [_ group_scope nt_group_presentation].
-Arguments Scope iso [_ group_scope nt_group_presentation].
+Arguments Generator _%nt_group_presentation.
+Arguments hom _ _%group_scope _%nt_group_presentation.
+Arguments  iso _ _%group_scope _%nt_group_presentation.
 
 Notation "x : p" := (Generator (x : p)) : group_presentation.
 
diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v
index 99d1aef..06feab2 100644
--- a/mathcomp/fingroup/quotient.v
+++ b/mathcomp/fingroup/quotient.v
@@ -198,9 +198,9 @@ Lemma quotientE : quotient = coset @* Q. Proof. by []. Qed.
 
 End Cosets.
 
-Arguments Scope coset_of [_ group_scope].
-Arguments Scope coset [_ group_scope group_scope].
-Arguments Scope quotient [_ group_scope group_scope].
+Arguments coset_of _ _%g.
+Arguments coset _ _%g _%g.
+Arguments quotient _ _%g _%g.
 Prenex Implicits coset_of coset.
 
 Bind Scope group_scope with coset_of.
diff --git a/mathcomp/odd_order/PFsection3.v b/mathcomp/odd_order/PFsection3.v
index 3c62a9e..e229772 100644
--- a/mathcomp/odd_order/PFsection3.v
+++ b/mathcomp/odd_order/PFsection3.v
@@ -206,10 +206,10 @@ Notation x7 := +x7. Notation x8 := +x8.
 Definition AndLit kvs kv := kv :: kvs.
 Definition AddLit := AndLit.
 Notation "(*dummy*)" := (Prop Prop) (at level 0) : defclause_scope.
-Arguments Scope AddLit [defclause_scope _].
+Arguments AddLit _%defclause_scope _.
 Infix "+" := AddLit : defclause_scope.
 Definition SubLit kvs kv := AddLit kvs (kv.1, - kv.2).
-Arguments Scope SubLit [defclause_scope _].
+Arguments SubLit _%defclause_scope _.
 Infix "-" := SubLit : defclause_scope.
 Coercion LastLit kv := [:: kv].
 
@@ -226,7 +226,7 @@ Notation "& kv1 , .. , kvn 'in' ij" :=
 Notation "& ? 'in' ij" := (Clause ij nil)
   (at level 200, ij at level 0, format "&  ?  'in'  ij").
 Definition DefClause := Clause.
-Arguments Scope DefClause [_ defclause_scope].
+Arguments DefClause _ _%defclause_scope.
 Notation "& ij = kvs" := (DefClause ij kvs)
   (at level 200, ij at level 0, format "&  ij  =  kvs").
 
diff --git a/mathcomp/odd_order/PFsection4.v b/mathcomp/odd_order/PFsection4.v
index 2be2adb..3cdff96 100644
--- a/mathcomp/odd_order/PFsection4.v
+++ b/mathcomp/odd_order/PFsection4.v
@@ -148,8 +148,7 @@ Definition primeTI_hypothesis (L K W W1 W2 : {set gT}) of W1 \x W2 = W :=
 
 End Four_1_to_2.
 
-Arguments Scope primeTI_hypothesis
-  [_ group_scope group_scope group_scope _ group_scope group_scope].
+Arguments primeTI_hypothesis _ _%g _%g _%g _ _%g _%g.
 
 Section Four_3_to_5.
 
diff --git a/mathcomp/real_closed/ordered_qelim.v b/mathcomp/real_closed/ordered_qelim.v
index 5f4e7f5..e9f15f9 100644
--- a/mathcomp/real_closed/ordered_qelim.v
+++ b/mathcomp/real_closed/ordered_qelim.v
@@ -82,21 +82,22 @@ Prenex Implicits term_eq.
 
 Bind Scope oterm_scope with term.
 Bind Scope oterm_scope with formula.
-Arguments Scope Add [_ oterm_scope oterm_scope].
-Arguments Scope Opp [_ oterm_scope].
-Arguments Scope NatMul [_ oterm_scope nat_scope].
-Arguments Scope Mul [_ oterm_scope oterm_scope].
-Arguments Scope Mul [_ oterm_scope oterm_scope].
-Arguments Scope Inv [_ oterm_scope].
-Arguments Scope Exp [_ oterm_scope nat_scope].
-Arguments Scope Equal [_ oterm_scope oterm_scope].
-Arguments Scope Unit [_ oterm_scope].
-Arguments Scope And [_ oterm_scope oterm_scope].
-Arguments Scope Or [_ oterm_scope oterm_scope].
-Arguments Scope Implies [_ oterm_scope oterm_scope].
-Arguments Scope Not [_ oterm_scope].
-Arguments Scope Exists [_ nat_scope oterm_scope].
-Arguments Scope Forall [_ nat_scope oterm_scope].
+Delimit Scope oterm_scope with oT.
+Arguments Add _ _%oT _%oT.
+Arguments Opp _ _%oT.
+Arguments NatMul _ _%oT _%N.
+Arguments Mul _ _%oT _%oT.
+Arguments Mul _ _%oT _%oT.
+Arguments Inv _ _%oT.
+Arguments Exp _ _%oT _%N.
+Arguments Equal _ _%oT _%oT.
+Arguments Unit _ _%oT.
+Arguments And _ _%oT _%oT.
+Arguments Or _ _%oT _%oT.
+Arguments Implies _ _%oT _%oT.
+Arguments Not _ _%oT.
+Arguments Exists _ _%N _%oT.
+Arguments Forall _ _%N _%oT.
 
 Arguments Bool [T].
 Prenex Implicits Const Add Opp NatMul Mul Exp Bool Unit And Or Implies Not.
@@ -105,7 +106,6 @@ Prenex Implicits Exists Forall Lt.
 Notation True := (Bool true).
 Notation False := (Bool false).
 
-Delimit Scope oterm_scope with oT.
 Notation "''X_' i" := (Var _ i) : oterm_scope.
 Notation "n %:R" := (NatConst _ n) : oterm_scope.
 Notation "x %:T" := (Const x) : oterm_scope.
diff --git a/mathcomp/real_closed/qe_rcf.v b/mathcomp/real_closed/qe_rcf.v
index c2e0333..743ca81 100644
--- a/mathcomp/real_closed/qe_rcf.v
+++ b/mathcomp/real_closed/qe_rcf.v
@@ -102,17 +102,18 @@ End QF.
 
 Bind Scope qf_scope with term.
 Bind Scope qf_scope with formula.
-Arguments Scope Add [_ qf_scope qf_scope].
-Arguments Scope Opp [_ qf_scope].
-Arguments Scope NatMul [_ qf_scope nat_scope].
-Arguments Scope Mul [_ qf_scope qf_scope].
-Arguments Scope Mul [_ qf_scope qf_scope].
-Arguments Scope Exp [_ qf_scope nat_scope].
-Arguments Scope Equal [_ qf_scope qf_scope].
-Arguments Scope And [_ qf_scope qf_scope].
-Arguments Scope Or [_ qf_scope qf_scope].
-Arguments Scope Implies [_ qf_scope qf_scope].
-Arguments Scope Not [_ qf_scope].
+Delimit Scope qf_scope with qfT.
+Arguments Add _ _%qfT _%qfT.
+Arguments Opp _ _%qfT.
+Arguments NatMul _ _%qfT _%N.
+Arguments Mul _ _%qfT _%qfT.
+Arguments Mul _ _%qfT _%qfT.
+Arguments Exp _ _%qfT _%N.
+Arguments Equal _ _%qfT _%qfT.
+Arguments And _ _%qfT _%qfT.
+Arguments Or _ _%qfT _%qfT.
+Arguments Implies _ _%qfT _%qfT.
+Arguments Not _ _%qfT.
 
 Arguments Bool [R].
 Prenex Implicits Const Add Opp NatMul Mul Exp Bool Unit And Or Implies Not Lt.
@@ -121,7 +122,6 @@ Prenex Implicits to_rterm.
 Notation True := (Bool true).
 Notation False := (Bool false).
 
-Delimit Scope qf_scope with qfT.
 Notation "''X_' i" := (Var _ i) : qf_scope.
 Notation "n %:R" := (NatConst _ n) : qf_scope.
 Notation "x %:T" := (Const x) : qf_scope.
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v
index f3ff7c3..7ca0bdb 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 Scope exponent [_ group_scope].
-Arguments Scope abelem [_ nat_scope group_scope].
-Arguments Scope is_abelem [_ group_scope].
-Arguments Scope pElem [_ nat_scope group_scope].
-Arguments Scope pnElem [_ nat_scope nat_scope group_scope].
-Arguments Scope nElem [_ nat_scope group_scope].
-Arguments Scope pmaxElem [_ nat_scope group_scope].
-Arguments Scope p_rank [_ nat_scope group_scope].
-Arguments Scope rank [_ group_scope].
-Arguments Scope gen_rank [_ group_scope].
+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.
 
 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 Scope Ohm [nat_scope _ group_scope].
-Arguments Scope Ohm_group [nat_scope _ group_scope].
-Arguments Scope Mho [nat_scope _ group_scope].
-Arguments Scope Mho_group [nat_scope _ group_scope].
+Arguments Ohm _%N _ _%g.
+Arguments Ohm_group _%N _ _%g.
+Arguments Mho _%N _ _%g.
+Arguments Mho_group _%N _ _%g.
 Arguments OhmPredP [n gT x].
 
 Notation "''Ohm_' n ( G )" := (Ohm n G)
@@ -2023,8 +2023,8 @@ Qed.
 
 End AbelianStructure.
 
-Arguments Scope abelian_type [_ group_scope].
-Arguments Scope homocyclic [_ group_scope].
+Arguments abelian_type _ _%g.
+Arguments homocyclic _ _%g.
 Prenex Implicits abelian_type homocyclic.
 
 Section IsogAbelian.
diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v
index c461a9e..f984960 100644
--- a/mathcomp/solvable/center.v
+++ b/mathcomp/solvable/center.v
@@ -56,7 +56,7 @@ Canonical center_group (G : {group gT}) : {group gT} :=
 
 End Defs.
 
-Arguments Scope center [_ group_scope].
+Arguments center _ _%g.
 Notation "''Z' ( A )" := (center A) : group_scope.
 Notation "''Z' ( H )" := (center_group H) : Group_scope.
 
diff --git a/mathcomp/solvable/commutator.v b/mathcomp/solvable/commutator.v
index 6a390ce..ffb07d2 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 Scope derived_at [nat_scope _ group_scope].
+Arguments derived_at _%N _ _%g.
 Notation "G ^` ( n )" := (derived_at n G) : group_scope.
 
 Section DerivedBasics.
diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v
index 7663163..bed8c5c 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 Scope cyclic [_ group_scope].
-Arguments Scope generator [_ group_scope group_scope].
-Arguments Scope expg_invn [_ group_scope nat_scope].
+Arguments cyclic _ _%g.
+Arguments generator _ _%g _%g.
+Arguments expg_invn _ _%g _%N.
 Arguments cyclicP [gT A].
 Prenex Implicits cyclic Zpm generator expg_invn.
 
@@ -556,7 +556,7 @@ Qed.
 
 End Metacyclic.
 
-Arguments Scope metacyclic [_ group_scope].
+Arguments metacyclic _ _%g.
 Prenex Implicits metacyclic.
 Arguments metacyclicP [gT A].
 
diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v
index 3416587..eb7ceab 100644
--- a/mathcomp/solvable/frobenius.v
+++ b/mathcomp/solvable/frobenius.v
@@ -98,17 +98,15 @@ CoInductive has_Frobenius_action G H : Prop :=
 
 End Definitions.
 
-Arguments Scope semiregular [_ group_scope group_scope].
-Arguments Scope semiprime [_ group_scope group_scope].
-Arguments Scope normedTI [_ group_scope group_scope group_scope].
-Arguments Scope Frobenius_group_with_complement [_ group_scope group_scope].
-Arguments Scope Frobenius_group [_ group_scope].
-Arguments Scope Frobenius_group_with_kernel [_ group_scope group_scope].
-Arguments Scope Frobenius_group_with_kernel_and_complement
-  [_ group_scope group_scope group_scope].
-Arguments Scope Frobenius_action
-  [_ group_scope group_scope _ group_scope action_scope].
-Arguments Scope has_Frobenius_action [_ group_scope group_scope].
+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.
 
 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 1dc6a35..c5b5c0c 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 Scope subnormal [_ group_scope group_scope].
-Arguments Scope invariant_factor [_ group_scope group_scope group_scope].
-Arguments Scope stable_factor [_ group_scope group_scope group_scope].
-Arguments Scope central_factor [_ group_scope group_scope group_scope].
-Arguments Scope maximal [_ group_scope group_scope].
-Arguments Scope maximal_eq [_ group_scope group_scope].
-Arguments Scope maxnormal [_ group_scope group_scope group_scope].
-Arguments Scope minnormal [_ group_scope group_scope].
-Arguments Scope simple [_ group_scope].
-Arguments Scope chief_factor [_ group_scope group_scope group_scope].
+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.
 Prenex Implicits subnormal maximal simple.
 
 Notation "H <|<| G" := (subnormal H G)
@@ -95,7 +95,7 @@ Notation "A .-central" := (central_factor A)
 Notation "G .-chief" := (chief_factor G)
   (at level 2, format "G .-chief") : group_rel_scope.
 
-Arguments Scope group_rel_of [_ group_rel_scope Group_scope Group_scope].
+Arguments group_rel_of _ _%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 7f60bed..91cc709 100644
--- a/mathcomp/solvable/jordanholder.v
+++ b/mathcomp/solvable/jordanholder.v
@@ -475,10 +475,8 @@ Qed.
 
 End StableCompositionSeries.
 
-Arguments Scope maxainv
-   [_ _ Group_scope Group_scope groupAction_scope group_scope group_scope].
-Arguments Scope asimple
-  [_ _ Group_scope Group_scope groupAction_scope group_scope].
+Arguments maxainv _ _ _%G _%G _%gact _%g _%g.
+Arguments asimple _ _ _%G _%G _%gact _%g.
 
 Section StrongJordanHolder.
 
diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v
index 06cf329..c1a2eb5 100644
--- a/mathcomp/solvable/maximal.v
+++ b/mathcomp/solvable/maximal.v
@@ -102,14 +102,14 @@ Definition SCN_at n B := [set A in SCN B | n <= 'r(A)].
 
 End Defs.
 
-Arguments Scope charsimple [_ group_scope].
-Arguments Scope Frattini [_ group_scope].
-Arguments Scope Fitting [_ group_scope].
-Arguments Scope critical [_ group_scope group_scope].
-Arguments Scope special [_ group_scope].
-Arguments Scope extraspecial [_ group_scope].
-Arguments Scope SCN [_ group_scope].
-Arguments Scope SCN_at [_ nat_scope group_scope].
+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.
 
diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v
index 3d9739d..387ce34 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 Scope lower_central_at [nat_scope _ group_scope].
-Arguments Scope upper_central_at [nat_scope _ group_scope].
+Arguments lower_central_at _%N _ _%g.
+Arguments upper_central_at _%N _ _%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 Scope nilpotent [_ group_scope].
-Arguments Scope nil_class [_ group_scope].
-Arguments Scope solvable [_ group_scope].
+Arguments nilpotent _ _%g.
+Arguments nil_class _ _%g.
+Arguments solvable _ _%g.
 Prenex Implicits nil_class nilpotent solvable.
 
 Section NilpotentProps.
diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v
index d383aa7..6507160 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 Scope pgroup [_ nat_scope group_scope].
-Arguments Scope psubgroup [_ nat_scope group_scope group_scope].
-Arguments Scope p_group [_ group_scope].
-Arguments Scope p_elt [_ nat_scope].
-Arguments Scope constt [_ group_scope nat_scope].
-Arguments Scope Hall [_ group_scope group_scope].
-Arguments Scope pHall [_ nat_scope group_scope group_scope].
-Arguments Scope Syl [_ nat_scope group_scope].
-Arguments Scope Sylow [_ group_scope group_scope].
+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.
 Prenex Implicits p_group Hall Sylow.
 
 Notation "pi .-group" := (pgroup pi)
@@ -863,8 +863,8 @@ Canonical pcore_group : {group gT} := Eval hnf in [group of pcore].
 
 End PcoreDef.
 
-Arguments Scope pcore [_ nat_scope group_scope].
-Arguments Scope pcore_group [_ nat_scope Group_scope].
+Arguments pcore _ _%N _%g.
+Arguments pcore_group _ _%N _%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.
@@ -886,7 +886,7 @@ Canonical pseries_group : {group gT} := group pseries_group_set.
 
 End PseriesDefs.
 
-Arguments Scope pseries [_ seq_scope group_scope].
+Arguments pseries _ _%SEQ _%g.
 Local Notation ConsPred p := (@Cons nat_pred p%N) (only parsing).
 Notation "''O_{' p1 , .. , pn } ( A )" :=
   (pseries (ConsPred p1 .. (ConsPred pn [::]) ..) A)
diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v
index c0ab34b..58a5f20 100644
--- a/mathcomp/solvable/primitive_action.v
+++ b/mathcomp/solvable/primitive_action.v
@@ -43,9 +43,8 @@ Definition primitive :=
 
 End PrimitiveDef.
 
-Arguments Scope imprimitivity_system
-  [_ _ group_scope group_scope action_scope group_scope].
-Arguments Scope primitive [_ _ group_scope group_scope action_scope].
+Arguments imprimitivity_system _ _ _%g _%g _%act _%g.
+Arguments primitive _ _ _%g _%g _%act.
 
 Notation "[ 'primitive' A , 'on' S | to ]" := (primitive A S to)
   (at level 0, format "[ 'primitive'  A ,  'on'  S  |  to ]") : form_scope.
@@ -184,9 +183,8 @@ Qed.
 
 End NTransitive.
 
-Arguments Scope dtuple_on [_ nat_scope group_scope].
-Arguments Scope ntransitive
-  [_ _ nat_scope group_scope group_scope action_scope].
+Arguments dtuple_on _ _%N _%g.
+Arguments ntransitive _ _ _%N _%g _%g _%act.
 Arguments n_act [gT sT] _ [n].
 
 Notation "n .-dtuple ( S )" := (dtuple_on n S)
diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v
index 8925b7d..dd45afa 100644
--- a/mathcomp/solvable/sylow.v
+++ b/mathcomp/solvable/sylow.v
@@ -535,7 +535,7 @@ Qed.
 
 End Zgroups.
 
-Arguments Scope Zgroup [_ group_scope].
+Arguments Zgroup _ _%g.
 Prenex Implicits Zgroup.
 
 Section NilPGroups.
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 9772b84..159c00e 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -436,7 +436,7 @@ Notation "x |-> y" := (FunDelta x y)
    format "'[hv' x '/ '  |->  y ']'") : fun_delta_scope.
 
 Delimit Scope fun_delta_scope with FUN_DELTA.
-Arguments Scope app_fdelta [_ type_scope fun_delta_scope _ _].
+Arguments app_fdelta _ _%type _%FUN_DELTA _ _.
 
 Notation "[ 'fun' z : T => F 'with' d1 , .. , dn ]" :=
   (SimplFunDelta (fun z : T =>
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 3f99e9f..4ff769e 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 Scope finfun_of_set [_ set_scope].
+Arguments finfun_of_set _ _%SET.
 
 Notation "{ 'set' T }" := (set_of (Phant T))
   (at level 0, format "{ 'set'  T }") : type_scope.
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index c1bf999..4347983 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -169,7 +169,7 @@ Notation Cons T := (@cons T) (only parsing).
 Notation Nil T := (@nil T) (only parsing).
 
 Bind Scope seq_scope with list.
-Arguments Scope cons [type_scope _ seq_scope].
+Arguments cons _%type _ _%SEQ.
 
 (* As :: and ++ are (improperly) declared in Init.datatypes, we only rebind   *)
 (* them here.                                                                 *)