Change deprecated Arguments Scope to Arguments

6 files changed, 49 insertions, 72 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.