Change deprecated Arguments Scope to Arguments

1 files changed, 19 insertions, 19 deletions

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.