Change Implicit Arguments to Arguments in real_closed

4 files changed, 26 insertions, 26 deletions

diff --git a/mathcomp/real_closed/mxtens.v b/mathcomp/real_closed/mxtens.v
index 4e6b72a..792e223 100644
--- a/mathcomp/real_closed/mxtens.v
+++ b/mathcomp/real_closed/mxtens.v
@@ -44,8 +44,8 @@ Proof. by rewrite ltn_mod; case: n k=> //; rewrite muln0=> [] []. Qed.
 Definition mxtens_unindex m n k :=
   (Ordinal (@mxtens_index_proof1 m n k), Ordinal (@mxtens_index_proof2 m n k)).
 
-Implicit Arguments mxtens_index [[m] [n]].
-Implicit Arguments mxtens_unindex [[m] [n]].
+Arguments mxtens_index {m n}.
+Arguments mxtens_unindex {m n}.
 
 Lemma mxtens_indexK m n : cancel (@mxtens_index m n) (@mxtens_unindex m n).
 Proof.
diff --git a/mathcomp/real_closed/ordered_qelim.v b/mathcomp/real_closed/ordered_qelim.v
index 4779540..5f4e7f5 100644
--- a/mathcomp/real_closed/ordered_qelim.v
+++ b/mathcomp/real_closed/ordered_qelim.v
@@ -76,7 +76,7 @@ Canonical term_eqMixin (T : eqType) := EqMixin (@term_eqP T).
 Canonical term_eqType (T : eqType) :=
    Eval hnf in EqType (term T) (@term_eqMixin T).
 
-Implicit Arguments term_eqP [x y].
+Arguments term_eqP T [x y].
 Prenex Implicits term_eq.
 
 
@@ -98,7 +98,7 @@ Arguments Scope Not [_ oterm_scope].
 Arguments Scope Exists [_ nat_scope oterm_scope].
 Arguments Scope Forall [_ nat_scope oterm_scope].
 
-Implicit Arguments Bool [T].
+Arguments Bool [T].
 Prenex Implicits Const Add Opp NatMul Mul Exp Bool Unit And Or Implies Not.
 Prenex Implicits Exists Forall Lt.
 
@@ -199,7 +199,7 @@ Canonical oclause_eqMixin (T : eqType) := EqMixin (@oclause_eqP T).
 Canonical oclause_eqType (T : eqType) :=
    Eval hnf in EqType (oclause T) (@oclause_eqMixin T).
 
-Implicit Arguments oclause_eqP [x y].
+Arguments oclause_eqP T [x y].
 Prenex Implicits oclause_eq.
 
 Section EvalTerm.
diff --git a/mathcomp/real_closed/qe_rcf.v b/mathcomp/real_closed/qe_rcf.v
index 272c44a..c2e0333 100644
--- a/mathcomp/real_closed/qe_rcf.v
+++ b/mathcomp/real_closed/qe_rcf.v
@@ -114,7 +114,7 @@ Arguments Scope Or [_ qf_scope qf_scope].
 Arguments Scope Implies [_ qf_scope qf_scope].
 Arguments Scope Not [_ qf_scope].
 
-Implicit Arguments Bool [R].
+Arguments Bool [R].
 Prenex Implicits Const Add Opp NatMul Mul Exp Bool Unit And Or Implies Not Lt.
 Prenex Implicits to_rterm.
 
@@ -537,7 +537,7 @@ rewrite lead_coefDl ?lead_coefMX ?size_mulX // ltnS size_polyC.
 by rewrite (leq_trans (leq_b1 _)) // size_poly_gt0.
 Qed.
 
-Implicit Arguments eval_LeadCoef [e p k].
+Arguments eval_LeadCoef [e p k].
 Prenex Implicits eval_LeadCoef.
 
 Lemma eval_AmulXn a n e : eval_poly e (AmulXn a n) = (eval e a)%:P * 'X^n.
@@ -625,7 +625,7 @@ rewrite (ihps _ (fun ps => k' (eval e lp :: ps))) => //= lps.
 by rewrite Pk.
 Qed.
 
-Implicit Arguments eval_SeqPInfty [e ps k].
+Arguments eval_SeqPInfty [e ps k].
 Prenex Implicits eval_SeqPInfty.
 
 Lemma eval_SeqMInfty e ps k k' :
@@ -640,7 +640,7 @@ rewrite eval_Size /= /k'' {k''}.
 by set X := map _ _; grab_eq k'' X; apply: ihps => {X} lps; rewrite Pk.
 Qed.
 
-Implicit Arguments eval_SeqMInfty [e ps k].
+Arguments eval_SeqMInfty [e ps k].
 Prenex Implicits eval_SeqMInfty.
 
 Lemma eval_ChangesPoly e ps k : qf_eval e (ChangesPoly ps k) =
@@ -682,7 +682,7 @@ set X := lead_coef _; grab_eq k'' X; apply: eval_LeadCoef => {X}.
 by move=> x; rewrite ihn // !eval_OpPoly /= !mul_polyC.
 Qed.
 
-Implicit Arguments eval_Rediv_rec_loop [e q sq cq c qq r n k].
+Arguments eval_Rediv_rec_loop [e q sq cq c qq r n k].
 Prenex Implicits eval_Rediv_rec_loop.
 
 Lemma eval_Rediv e p q k k' (d := (redivp (eval_poly e p) (eval_poly e q))) :
@@ -698,7 +698,7 @@ rewrite (eval_LeadCoef (fun lq =>
 by rewrite redivp_rec_loopP.
 Qed.
 
-Implicit Arguments eval_Rediv [e p q k].
+Arguments eval_Rediv [e p q k].
 Prenex Implicits eval_Rediv.
 
 Lemma eval_NextMod e p q k k' :
@@ -716,7 +716,7 @@ rewrite (eval_Rediv (fun mpq =>
 by rewrite Pk !eval_OpPoly.
 Qed.
 
-Implicit Arguments eval_NextMod [e p q k].
+Arguments eval_NextMod [e p q k].
 Prenex Implicits eval_NextMod.
 
 Lemma eval_Rgcd_loop e n p q k k' :
@@ -759,7 +759,7 @@ rewrite big_cons (ihsp _ (fun r => k' (rgcdp (eval_poly e p) r))) //.
 by move=> r; apply: eval_Rgcd.
 Qed.
 
-Implicit Arguments eval_Rgcd [e p q k].
+Arguments eval_Rgcd [e p q k].
 Prenex Implicits eval_Rgcd.
 
 
@@ -781,7 +781,7 @@ rewrite (eval_NextMod (fun npq => k' (p' :: mods_aux q' npq n))) => // npq.
 by rewrite (ihn _ _ _ (fun ps => k' (p' :: ps))) => // ps; rewrite Pk.
 Qed.
 
-Implicit Arguments eval_ModsAux [e p q n k].
+Arguments eval_ModsAux [e p q n k].
 Prenex Implicits eval_ModsAux.
 
 Lemma eval_Mods e p q k k' :
@@ -789,7 +789,7 @@ Lemma eval_Mods e p q k k' :
   qf_eval e (Mods p q k) = k' (mods (eval_poly e p) (eval_poly e q)).
 Proof. by move=> Pk; rewrite !eval_Size; apply: eval_ModsAux. Qed.
 
-Implicit Arguments eval_Mods [e p q k].
+Arguments eval_Mods [e p q k].
 Prenex Implicits eval_Mods.
 
 Lemma eval_TaqR e p q k :
@@ -831,7 +831,7 @@ Lemma eval_TaqsR e p sq i k k' :
   k' (taqsR (eval_poly e p) (map (eval_poly e) sq) i).
 Proof. by move=> Pk; rewrite /TaqsR /taqsR eval_TaqR Pk /= eval_Pcq. Qed.
 
-Implicit Arguments eval_TaqsR [e p sq i k].
+Arguments eval_TaqsR [e p sq i k].
 Prenex Implicits eval_TaqsR.
 
 Fact invmx_ctmat1 : invmx (map_mx (intr : int -> F) ctmat1) =
@@ -885,7 +885,7 @@ rewrite (eval_TaqsR
 by move=> y; rewrite (ihn _ k') // -(eval_Coefs e).
 Qed.
 
-Implicit Arguments eval_CcountWeak [e p sq k].
+Arguments eval_CcountWeak [e p sq k].
 Prenex Implicits eval_CcountWeak.
 
 Lemma eval_ProdPoly e T s f k f' k' :
@@ -902,7 +902,7 @@ move=> fa; rewrite (ihs _ (fun fs => k' (eval_poly e fa * fs))) //.
 by move=> fs; rewrite Pk eval_OpPoly.
 Qed.
 
-Implicit Arguments eval_ProdPoly [e T s f k].
+Arguments eval_ProdPoly [e T s f k].
 Prenex Implicits eval_ProdPoly.
 
 Lemma eval_BoundingPoly e sq :
diff --git a/mathcomp/real_closed/realalg.v b/mathcomp/real_closed/realalg.v
index 0cbba9f..7d9d987 100644
--- a/mathcomp/real_closed/realalg.v
+++ b/mathcomp/real_closed/realalg.v
@@ -194,11 +194,11 @@ Definition eq_algcreal : rel algcreal := eq_algcreal_dec.
 
 Lemma eq_algcrealP (x y : algcreal) : reflect (x == y)%CR (eq_algcreal x y).
 Proof. by rewrite /eq_algcreal; case: eq_algcreal_dec=> /=; constructor. Qed.
-Implicit Arguments eq_algcrealP [x y].
+Arguments eq_algcrealP [x y].
 
 Lemma neq_algcrealP (x y : algcreal) : reflect (x != y)%CR (~~ eq_algcreal x y).
 Proof. by rewrite /eq_algcreal; case: eq_algcreal_dec=> /=; constructor. Qed.
-Implicit Arguments neq_algcrealP [x y].
+Arguments neq_algcrealP [x y].
 Prenex Implicits eq_algcrealP neq_algcrealP.
 
 Fact eq_algcreal_is_equiv : equiv_class_of eq_algcreal.
@@ -284,11 +284,11 @@ Definition le_algcreal : rel algcreal := fun x y => ~~ ltVge_algcreal_dec y x.
 
 Lemma lt_algcrealP (x y : algcreal) : reflect (x < y)%CR (lt_algcreal x y).
 Proof. by rewrite /lt_algcreal; case: ltVge_algcreal_dec; constructor. Qed.
-Implicit Arguments lt_algcrealP [x y].
+Arguments lt_algcrealP [x y].
 
 Lemma le_algcrealP (x y : algcreal) : reflect (x <= y)%CR (le_algcreal x y).
 Proof. by rewrite /le_algcreal; case: ltVge_algcreal_dec; constructor. Qed.
-Implicit Arguments le_algcrealP [x y].
+Arguments le_algcrealP [x y].
 Prenex Implicits lt_algcrealP le_algcrealP.
 
 Definition exp_algcreal x n := iterop n mul_algcreal x one_algcreal.
@@ -609,7 +609,7 @@ Qed.
 
 Lemma nequiv_alg (x y : algcreal) : reflect (x != y)%CR (x != y %[mod {alg F}]).
 Proof. by rewrite eqquotE; apply: neq_algcrealP. Qed.
-Implicit Arguments nequiv_alg [x y].
+Arguments nequiv_alg [x y].
 Prenex Implicits nequiv_alg.
 
 Lemma pi_algK (x : algcreal) : (repr (\pi_{alg F} x) == x)%CR.
@@ -711,7 +711,7 @@ elim/quotW=> x; elim/quotW=> y; elim/quotW=> z; rewrite !piE -equiv_alg /=.
 by apply: eq_crealP; exists m0=> * /=; rewrite mulrDl subrr normr0.
 Qed.
 
-Implicit Arguments neq_creal_cst [F x y].
+Arguments neq_creal_cst [F x y].
 Prenex Implicits neq_creal_cst.
 
 Lemma nonzero1_alg : one_alg != zero_alg.
@@ -964,11 +964,11 @@ Proof. by rewrite [`|_|]piE. Qed.
 
 Lemma lt_algP (x y : algcreal) : reflect (x < y)%CR (\pi_{alg F} x < \pi y).
 Proof. by rewrite lt_pi; apply: lt_algcrealP. Qed.
-Implicit Arguments lt_algP [x y].
+Arguments lt_algP [x y].
 
 Lemma le_algP (x y : algcreal) : reflect (x <= y)%CR (\pi_{alg F} x <= \pi y).
 Proof. by rewrite le_pi; apply: le_algcrealP. Qed.
-Implicit Arguments le_algP [x y].
+Arguments le_algP [x y].
 Prenex Implicits lt_algP le_algP.
 
 Lemma ler_to_alg : {mono to_alg : x y / x <= y}.