Change deprecated Arguments Scope to Arguments

12 files changed, 74 insertions, 80 deletions

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.