From 2525c33691e25f837b7dca31d4c702199b3dbc5d Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Sun, 4 Mar 2018 16:57:06 -0800
Subject: Change deprecated Arguments Scope to Arguments

---
 mathcomp/odd_order/PFsection3.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'mathcomp/odd_order/PFsection3.v')

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").
 
-- 
cgit v1.2.3