Change deprecated Arguments Scope to Arguments

2 files changed, 4 insertions, 5 deletions

diff --git a/mathcomp/odd_order/PFsection3.v b/mathcomp/odd_order/PFsection3.v
index 3c62a9e..e229772 100644
--- a/mathcomp/odd_order/PFsection3.v
+++ b/mathcomp/odd_order/PFsection3.v
@@ -206,10 +206,10 @@ Notation x7 := +x7. Notation x8 := +x8.
 Definition AndLit kvs kv := kv :: kvs.
 Definition AddLit := AndLit.
 Notation "(*dummy*)" := (Prop Prop) (at level 0) : defclause_scope.
-Arguments Scope AddLit [defclause_scope _].
+Arguments AddLit _%defclause_scope _.
 Infix "+" := AddLit : defclause_scope.
 Definition SubLit kvs kv := AddLit kvs (kv.1, - kv.2).
-Arguments Scope SubLit [defclause_scope _].
+Arguments SubLit _%defclause_scope _.
 Infix "-" := SubLit : defclause_scope.
 Coercion LastLit kv := [:: kv].
 
@@ -226,7 +226,7 @@ Notation "& kv1 , .. , kvn 'in' ij" :=
 Notation "& ? 'in' ij" := (Clause ij nil)
   (at level 200, ij at level 0, format "&  ?  'in'  ij").
 Definition DefClause := Clause.
-Arguments Scope DefClause [_ defclause_scope].
+Arguments DefClause _ _%defclause_scope.
 Notation "& ij = kvs" := (DefClause ij kvs)
   (at level 200, ij at level 0, format "&  ij  =  kvs").
 
diff --git a/mathcomp/odd_order/PFsection4.v b/mathcomp/odd_order/PFsection4.v
index 2be2adb..3cdff96 100644
--- a/mathcomp/odd_order/PFsection4.v
+++ b/mathcomp/odd_order/PFsection4.v
@@ -148,8 +148,7 @@ Definition primeTI_hypothesis (L K W W1 W2 : {set gT}) of W1 \x W2 = W :=
 
 End Four_1_to_2.
 
-Arguments Scope primeTI_hypothesis
-  [_ group_scope group_scope group_scope _ group_scope group_scope].
+Arguments primeTI_hypothesis _ _%g _%g _%g _ _%g _%g.
 
 Section Four_3_to_5.