Change deprecated Arguments Scope to Arguments

2 files changed, 28 insertions, 28 deletions

diff --git a/mathcomp/real_closed/ordered_qelim.v b/mathcomp/real_closed/ordered_qelim.v
index 5f4e7f5..e9f15f9 100644
--- a/mathcomp/real_closed/ordered_qelim.v
+++ b/mathcomp/real_closed/ordered_qelim.v
@@ -82,21 +82,22 @@ Prenex Implicits term_eq.
 
 Bind Scope oterm_scope with term.
 Bind Scope oterm_scope with formula.
-Arguments Scope Add [_ oterm_scope oterm_scope].
-Arguments Scope Opp [_ oterm_scope].
-Arguments Scope NatMul [_ oterm_scope nat_scope].
-Arguments Scope Mul [_ oterm_scope oterm_scope].
-Arguments Scope Mul [_ oterm_scope oterm_scope].
-Arguments Scope Inv [_ oterm_scope].
-Arguments Scope Exp [_ oterm_scope nat_scope].
-Arguments Scope Equal [_ oterm_scope oterm_scope].
-Arguments Scope Unit [_ oterm_scope].
-Arguments Scope And [_ oterm_scope oterm_scope].
-Arguments Scope Or [_ oterm_scope oterm_scope].
-Arguments Scope Implies [_ oterm_scope oterm_scope].
-Arguments Scope Not [_ oterm_scope].
-Arguments Scope Exists [_ nat_scope oterm_scope].
-Arguments Scope Forall [_ nat_scope oterm_scope].
+Delimit Scope oterm_scope with oT.
+Arguments Add _ _%oT _%oT.
+Arguments Opp _ _%oT.
+Arguments NatMul _ _%oT _%N.
+Arguments Mul _ _%oT _%oT.
+Arguments Mul _ _%oT _%oT.
+Arguments Inv _ _%oT.
+Arguments Exp _ _%oT _%N.
+Arguments Equal _ _%oT _%oT.
+Arguments Unit _ _%oT.
+Arguments And _ _%oT _%oT.
+Arguments Or _ _%oT _%oT.
+Arguments Implies _ _%oT _%oT.
+Arguments Not _ _%oT.
+Arguments Exists _ _%N _%oT.
+Arguments Forall _ _%N _%oT.
 
 Arguments Bool [T].
 Prenex Implicits Const Add Opp NatMul Mul Exp Bool Unit And Or Implies Not.
@@ -105,7 +106,6 @@ Prenex Implicits Exists Forall Lt.
 Notation True := (Bool true).
 Notation False := (Bool false).
 
-Delimit Scope oterm_scope with oT.
 Notation "''X_' i" := (Var _ i) : oterm_scope.
 Notation "n %:R" := (NatConst _ n) : oterm_scope.
 Notation "x %:T" := (Const x) : oterm_scope.
diff --git a/mathcomp/real_closed/qe_rcf.v b/mathcomp/real_closed/qe_rcf.v
index c2e0333..743ca81 100644
--- a/mathcomp/real_closed/qe_rcf.v
+++ b/mathcomp/real_closed/qe_rcf.v
@@ -102,17 +102,18 @@ End QF.
 
 Bind Scope qf_scope with term.
 Bind Scope qf_scope with formula.
-Arguments Scope Add [_ qf_scope qf_scope].
-Arguments Scope Opp [_ qf_scope].
-Arguments Scope NatMul [_ qf_scope nat_scope].
-Arguments Scope Mul [_ qf_scope qf_scope].
-Arguments Scope Mul [_ qf_scope qf_scope].
-Arguments Scope Exp [_ qf_scope nat_scope].
-Arguments Scope Equal [_ qf_scope qf_scope].
-Arguments Scope And [_ qf_scope qf_scope].
-Arguments Scope Or [_ qf_scope qf_scope].
-Arguments Scope Implies [_ qf_scope qf_scope].
-Arguments Scope Not [_ qf_scope].
+Delimit Scope qf_scope with qfT.
+Arguments Add _ _%qfT _%qfT.
+Arguments Opp _ _%qfT.
+Arguments NatMul _ _%qfT _%N.
+Arguments Mul _ _%qfT _%qfT.
+Arguments Mul _ _%qfT _%qfT.
+Arguments Exp _ _%qfT _%N.
+Arguments Equal _ _%qfT _%qfT.
+Arguments And _ _%qfT _%qfT.
+Arguments Or _ _%qfT _%qfT.
+Arguments Implies _ _%qfT _%qfT.
+Arguments Not _ _%qfT.
 
 Arguments Bool [R].
 Prenex Implicits Const Add Opp NatMul Mul Exp Bool Unit And Or Implies Not Lt.
@@ -121,7 +122,6 @@ Prenex Implicits to_rterm.
 Notation True := (Bool true).
 Notation False := (Bool false).
 
-Delimit Scope qf_scope with qfT.
 Notation "''X_' i" := (Var _ i) : qf_scope.
 Notation "n %:R" := (NatConst _ n) : qf_scope.
 Notation "x %:T" := (Const x) : qf_scope.