Remplacement Import par Open Scope en v8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3909 85f007b7-540e-0410-9357-904b9bb8a0f7

44 files changed, 47 insertions, 47 deletions

diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v
index 36131beb0..60ab7b6cf 100644
--- a/theories/Reals/Alembert.v
+++ b/theories/Reals/Alembert.v
@@ -14,7 +14,7 @@ Require Rseries.
 Require SeqProp.
 Require PartSum.
 Require Max.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (***************************************************)
 (* Various versions of the criterion of D'Alembert *)
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index 7047bb03d..8de35273d 100644
--- a/theories/Reals/AltSeries.v
+++ b/theories/Reals/AltSeries.v
@@ -14,7 +14,7 @@ Require Rseries.
 Require SeqProp.
 Require PartSum.
 Require Max.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (**********)
 Definition tg_alt [Un:nat->R] : nat->R := [i:nat]``(pow (-1) i)*(Un i)``.
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index 62d160934..51970655a 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -12,7 +12,7 @@ Require Rbase.
 Require Rbasic_fun.
 Require Even.
 Require Div2.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Lemma minus_neq_O : (n,i:nat) (lt i n) -> ~(minus n i)=O.
 Intros; Red; Intro.
diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v
index 03b6b46fc..c90f121a9 100644
--- a/theories/Reals/Binomial.v
+++ b/theories/Reals/Binomial.v
@@ -11,7 +11,7 @@
 Require Rbase.
 Require Rfunctions.
 Require PartSum.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Definition C [n,p:nat] : R := ``(INR (fact n))/((INR (fact p))*(INR (fact (minus n p))))``.
 
diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v
index 5cd8bf672..bbb3c3396 100644
--- a/theories/Reals/Cauchy_prod.v
+++ b/theories/Reals/Cauchy_prod.v
@@ -12,7 +12,7 @@ Require Rbase.
 Require Rfunctions.
 Require Rseries.
 Require PartSum.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (**********)
 Lemma sum_N_predN : (An:nat->R;N:nat) (lt O N) -> (sum_f_R0 An N)==``(sum_f_R0 An (pred N)) + (An N)``.
diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index ae650225f..c89787feb 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -14,8 +14,8 @@ Require SeqSeries.
 Require Rtrigo_def.
 Require Cos_rel.
 Require Max.
-V7only [Import nat_scope.].
-V7only [Import R_scope.].
+V7only [Import nat_scope.]. Open Scope nat_scope.
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Definition Majxy [x,y:R] : nat->R := [n:nat](Rdiv (pow (Rmax R1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (4) (S n))) (INR (fact n))).
 
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index b773057ed..5196cba38 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -12,7 +12,7 @@ Require Rbase.
 Require Rfunctions.
 Require SeqSeries.
 Require Rtrigo_def.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Definition A1 [x:R] : nat->R := [N:nat](sum_f_R0 [k:nat]``(pow (-1) k)/(INR (fact (mult (S (S O)) k)))*(pow x (mult (S (S O)) k))`` N). 
  
diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index 62bf0265d..66a66f399 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -10,7 +10,7 @@
 
 Require RIneq.
 Require Omega.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Lemma Rlt_R0_R2 : ``0<2``.
 Replace ``2`` with (INR (2)); [Apply lt_INR_0; Apply lt_O_Sn | Reflexivity].
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index ca5de937b..34c9a2c50 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -17,7 +17,7 @@ Require PSeries_reg.
 Require Div2.
 Require Even.
 Require Max.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Definition E1 [x:R] : nat->R := [N:nat](sum_f_R0 [k:nat]``/(INR (fact k))*(pow x k)`` N).
 
diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v
index 7de5c64c0..3f06c65d8 100644
--- a/theories/Reals/MVT.v
+++ b/theories/Reals/MVT.v
@@ -12,7 +12,7 @@ Require Rbase.
 Require Rfunctions.
 Require Ranalysis1.
 Require Rtopology.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (* The Mean Value Theorem *)
 Theorem MVT : (f,g:R->R;a,b:R;pr1:(c:R)``a<c<b``->(derivable_pt f c);pr2:(c:R)``a<c<b``->(derivable_pt g c)) ``a<b`` -> ((c:R)``a<=c<=b``->(continuity_pt f c)) -> ((c:R)``a<=c<=b``->(continuity_pt g c)) -> (EXT c : R | (EXT P : ``a<c<b`` | ``((g b)-(g a))*(derive_pt f c (pr1 c P))==((f b)-(f a))*(derive_pt g c (pr2 c P))``)).
diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v
index 7c7cb59ea..5878481a5 100644
--- a/theories/Reals/NewtonInt.v
+++ b/theories/Reals/NewtonInt.v
@@ -13,7 +13,7 @@ Require Rfunctions.
 Require SeqSeries.
 Require Rtrigo.
 Require Ranalysis.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (*******************************************)
 (*            Newton's Integral            *)
diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v
index 8a4aa1fc5..422cbcf6a 100644
--- a/theories/Reals/PSeries_reg.v
+++ b/theories/Reals/PSeries_reg.v
@@ -14,7 +14,7 @@ Require SeqSeries.
 Require Ranalysis1.
 Require Max.
 Require Even.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Definition Boule [x:R;r:posreal] : R -> Prop := [y:R]``(Rabsolu (y-x))<r``.
 
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index 66d3496d3..7f6bd9177 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -13,7 +13,7 @@ Require Rfunctions.
 Require Rseries.
 Require Rcomplete.
 Require Max.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Lemma tech1 : (An:nat->R;N:nat) ((n:nat)``(le n N)``->``0<(An n)``) -> ``0 < (sum_f_R0 An N)``.
 Intros; Induction N.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 0f57c281d..025eb5410 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -16,9 +16,9 @@ Require Export Raxioms.
 Require Export ZArithRing.
 Require Omega.
 Require Export Field.
-V7only [Import nat_scope.].
-V7only [Import Z_scope.].
-V7only [Import R_scope.].
+V7only [Import nat_scope.]. Open Scope nat_scope.
+V7only [Import Z_scope.]. Open Scope Z_scope.
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Implicit Variable Type r:R.
 
diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v
index edfb48728..00563ebcd 100644
--- a/theories/Reals/RList.v
+++ b/theories/Reals/RList.v
@@ -10,7 +10,7 @@
 
 Require Rbase.
 Require Rfunctions.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Inductive Rlist : Type :=
 | nil : Rlist
diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v
index 2fa84607f..f710c5120 100644
--- a/theories/Reals/R_sqr.v
+++ b/theories/Reals/R_sqr.v
@@ -10,7 +10,7 @@
 
 Require Rbase.
 Require Rbasic_fun.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (****************************************************)
 (* Rsqr : some results                              *)
diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v
index 0fd419288..c3997a312 100644
--- a/theories/Reals/R_sqrt.v
+++ b/theories/Reals/R_sqrt.v
@@ -11,7 +11,7 @@
 Require Rbase.
 Require Rfunctions.
 Require Rsqrt_def.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (* Here is a continuous extension of Rsqrt on R *)
 Definition sqrt : R->R := [x:R](Cases (case_Rabsolu x) of
diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v
index d467261c7..6e144928e 100644
--- a/theories/Reals/Ranalysis.v
+++ b/theories/Reals/Ranalysis.v
@@ -28,7 +28,7 @@ Require Export RList.
 Require Export Sqrt_reg.
 Require Export Ranalysis4.
 Require Export Rpower.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Axiom AppVar : R.
 
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index 2b883f7b6..aa41a8ae0 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -12,7 +12,7 @@ Require Rbase.
 Require Rfunctions.
 Require Export Rlimit.
 Require Export Rderiv.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 Implicit Variable Type f:R->R.
 
 (****************************************************)
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v
index 05cfabcba..d13e96668 100644
--- a/theories/Reals/Ranalysis2.v
+++ b/theories/Reals/Ranalysis2.v
@@ -11,7 +11,7 @@
 Require Rbase.
 Require Rfunctions.
 Require Ranalysis1.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (**********)
 Lemma formule : (x,h,l1,l2:R;f1,f2:R->R) ``h<>0`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ``((f1 (x+h))/(f2 (x+h))-(f1 x)/(f2 x))/h-(l1*(f2 x)-l2*(f1 x))/(Rsqr (f2 x))`` == ``/(f2 (x+h))*(((f1 (x+h))-(f1 x))/h-l1) + l1/((f2 x)*(f2 (x+h)))*((f2 x)-(f2 (x+h))) - (f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))-(f2 x))/h-l2) + (l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))*((f2 (x+h))-(f2 x))``.
diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v
index 35f28aa64..7137deac3 100644
--- a/theories/Reals/Ranalysis3.v
+++ b/theories/Reals/Ranalysis3.v
@@ -12,7 +12,7 @@ Require Rbase.
 Require Rfunctions.
 Require Ranalysis1.
 Require Ranalysis2.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (* Division *)
 Theorem derivable_pt_lim_div : (f1,f2:R->R;x,l1,l2:R) (derivable_pt_lim f1 x l1) -> (derivable_pt_lim f2 x l2) -> ~``(f2 x)==0``-> (derivable_pt_lim (div_fct f1 f2) x ``(l1*(f2 x)-l2*(f1 x))/(Rsqr (f2 x))``).
diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v
index 23c52c330..4da04bab8 100644
--- a/theories/Reals/Ranalysis4.v
+++ b/theories/Reals/Ranalysis4.v
@@ -15,7 +15,7 @@ Require Rtrigo.
 Require Ranalysis1.
 Require Ranalysis3.
 Require Exp_prop.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (**********)
 Lemma derivable_pt_inv : (f:R->R;x:R) ``(f x)<>0`` -> (derivable_pt f x) -> (derivable_pt (inv_fct f) x).
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 6775958fc..3d312634d 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -15,7 +15,7 @@
 Require Export ZArith_base.
 Require Export Rsyntax.
 Require Export TypeSyntax.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (*********************************************************)
 (*               Field axioms                            *)
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 0c173c951..71fa79ad2 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -16,7 +16,7 @@
 Require Rbase.
 Require R_Ifp.
 Require Fourier.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Implicit Variable Type r:R.
 
diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v
index e62db41e5..c9f2596aa 100644
--- a/theories/Reals/Rcomplete.v
+++ b/theories/Reals/Rcomplete.v
@@ -13,7 +13,7 @@ Require Rfunctions.
 Require Rseries.
 Require SeqProp.
 Require Max.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (****************************************************)
 (*              R is complete :                     *)
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v
index 392c299a0..d73c10168 100644
--- a/theories/Reals/Rderiv.v
+++ b/theories/Reals/Rderiv.v
@@ -20,7 +20,7 @@ Require Fourier.
 Require Classical_Prop.
 Require Classical_Pred_Type.
 Require Omega.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (*********)
 Definition D_x:(R->Prop)->R->R->Prop:=[D:R->Prop][y:R][x:R]
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 1131f1167..b7be1f077 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -25,7 +25,7 @@ Require Export SplitRmult.
 Require Export ArithProp.
 Require Omega.
 Require Zpower.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (*******************************)
 (**     Factorial              *)
diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v
index 831b32b9e..8168571e8 100644
--- a/theories/Reals/Rgeom.v
+++ b/theories/Reals/Rgeom.v
@@ -13,7 +13,7 @@ Require Rfunctions.
 Require SeqSeries.
 Require Rtrigo.
 Require R_sqrt.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Definition dist_euc [x0,y0,x1,y1:R] : R := ``(sqrt ((Rsqr (x0-x1))+(Rsqr (y0-y1))))``.
 
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v
index 55869a110..63322838a 100644
--- a/theories/Reals/RiemannInt.v
+++ b/theories/Reals/RiemannInt.v
@@ -16,7 +16,7 @@ Require RiemannInt_SF.
 Require Classical_Prop.
 Require Classical_Pred_Type.
 Require Max.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Implicit Arguments On.
 
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index 46157e3c9..d436e780f 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -12,7 +12,7 @@ Require Rbase.
 Require Rfunctions.
 Require Ranalysis.
 Require Classical_Prop.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Implicit Arguments On.
 
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 7f2baa8ef..f21ddcef9 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -17,7 +17,7 @@ Require Rbase.
 Require Rfunctions.
 Require Classical_Prop.
 Require Fourier.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (*******************************)
 (*      Calculus               *)
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index e76236a89..0c641c692 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -23,7 +23,7 @@ Require Rsqrt_def.
 Require R_sqrt.
 Require MVT.
 Require Ranalysis4.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Lemma P_Rmin: (P : R ->  Prop) (x, y : R) (P x) -> (P y) ->  (P (Rmin x y)).
 Intros P x y H1 H2; Unfold Rmin; Case (total_order_Rle x y); Intro; Assumption.
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v
index 24eba0cef..10dd8eb83 100644
--- a/theories/Reals/Rprod.v
+++ b/theories/Reals/Rprod.v
@@ -14,7 +14,7 @@ Require Rfunctions.
 Require Rseries.
 Require PartSum.
 Require Binomial.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (* TT Ak; 1<=k<=N *)
 Fixpoint prod_f_SO [An:nat->R;N:nat] : R := Cases N of
diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
index 4769c0cd2..f0cefb2e8 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.v
@@ -12,7 +12,7 @@ Require Rbase.
 Require Rfunctions.
 Require Rseries.
 Require PartSum.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Set Implicit Arguments.
 
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 8267692a6..2f11d3001 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -13,7 +13,7 @@ Require Rbase.
 Require Rfunctions.
 Require SeqSeries.
 Require Ranalysis1.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Fixpoint Dichotomy_lb [x,y:R;P:R->bool;N:nat] : R :=
 Cases N of 
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v
index 5dc510c66..c32e76ce2 100644
--- a/theories/Reals/Rtopology.v
+++ b/theories/Reals/Rtopology.v
@@ -14,7 +14,7 @@ Require Ranalysis1.
 Require RList.
 Require Classical_Prop.
 Require Classical_Pred_Type.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Definition included [D1,D2:R->Prop] : Prop := (x:R)(D1 x)->(D2 x).
 Definition disc [x:R;delta:posreal] : R->Prop := [y:R]``(Rabsolu (y-x))<delta``.
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 28a9fccb8..c2fbf5d32 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -19,7 +19,7 @@ Require Export Cos_plus.
 Require ZArith_base.
 Require Zcomplements.
 Require Classical_Prop.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (** sin_PI2 is the only remaining axiom **)
 Axiom sin_PI2 : ``(sin (PI/2))==1``.
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
index 1f8b0ad07..87dbc98b4 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -12,7 +12,7 @@ Require Rbase.
 Require Rfunctions.
 Require SeqSeries.
 Require Rtrigo_def.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (*****************************************************************)
 (* Using series definitions of cos and sin                       *)
diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v
index 925d7be95..52a1fa030 100644
--- a/theories/Reals/Rtrigo_calc.v
+++ b/theories/Reals/Rtrigo_calc.v
@@ -13,7 +13,7 @@ Require Rfunctions.
 Require SeqSeries.
 Require Rtrigo.
 Require R_sqrt.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Lemma tan_PI : ``(tan PI)==0``.
 Unfold tan; Rewrite sin_PI; Rewrite cos_PI; Unfold Rdiv; Apply Rmult_Ol. 
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v
index 8ede5a7a1..a2b2ebe05 100644
--- a/theories/Reals/Rtrigo_def.v
+++ b/theories/Reals/Rtrigo_def.v
@@ -13,7 +13,7 @@ Require Rfunctions.
 Require SeqSeries.
 Require Rtrigo_fun.
 Require Max.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (*****************************)
 (* Definition of exponential *)
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index 6ec18e56a..bc04d7470 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -14,7 +14,7 @@ Require SeqSeries.
 Require Rtrigo.
 Require Ranalysis1.
 Require PSeries_reg.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Lemma CVN_R_cos : (fn:nat->R->R) (fn == [N:nat][x:R]``(pow (-1) N)/(INR (fact (mult (S (S O)) N)))*(pow x (mult (S (S O)) N))``) -> (CVN_R fn).
 Unfold CVN_R; Intros.
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 3f1a84f9d..a49727b87 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -13,7 +13,7 @@ Require Rfunctions.
 Require Rseries.
 Require Classical.
 Require Max.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 Definition Un_decreasing [Un:nat->R] : Prop := (n:nat) (Rle (Un (S n)) (Un n)).
 Definition opp_seq [Un:nat->R] : nat->R := [n:nat]``-(Un n)``.
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v
index f3cc24ae9..d968112c5 100644
--- a/theories/Reals/SeqSeries.v
+++ b/theories/Reals/SeqSeries.v
@@ -21,7 +21,7 @@ Require Export Rsigma.
 Require Export Rprod.
 Require Export Cauchy_prod.
 Require Export Alembert.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (**********)
 Lemma sum_maj1 : (fn:nat->R->R;An:nat->R;x,l1,l2:R;N:nat) (Un_cv [n:nat](SP fn n x) l1) -> (Un_cv [n:nat](sum_f_R0 An n) l2) -> ((n:nat)``(Rabsolu (fn n x))<=(An n)``) -> ``(Rabsolu (l1-(SP fn N x)))<=l2-(sum_f_R0 An N)``.
diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v
index 7d282e592..859c95753 100644
--- a/theories/Reals/Sqrt_reg.v
+++ b/theories/Reals/Sqrt_reg.v
@@ -12,7 +12,7 @@ Require Rbase.
 Require Rfunctions.
 Require Ranalysis1.
 Require R_sqrt.
-V7only [Import R_scope.].
+V7only [Import R_scope.]. Open Scope R_scope.
 
 (**********)
 Lemma sqrt_var_maj : (h:R) ``(Rabsolu h) <= 1`` -> ``(Rabsolu ((sqrt (1+h))-1))<=(Rabsolu h)``.