Change deprecated Arguments Scope to Arguments

1 files changed, 9 insertions, 11 deletions

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)