Change deprecated Arguments Scope to Arguments

8 files changed, 88 insertions, 99 deletions

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.