Open Scope en Local

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

46 files changed, 52 insertions, 48 deletions

diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v
index 60ab7b6cf5..6745a3fc4c 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local Scope R_scope.
 
 (***************************************************)
 (* Various versions of the criterion of D'Alembert *)
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index 8de35273d7..b512f9beaf 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 51970655a6..db4494dd21 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -12,7 +12,8 @@ Require Rbase.
 Require Rbasic_fun.
 Require Even.
 Require Div2.
-V7only [Import R_scope.]. Open Scope R_scope.
+Open Local Scope Z_scope.
+V7only [Import R_scope.]. Open Local 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 c90f121a98..1751f82775 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 bbb3c33963..697316b84d 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 c89787febe..41815fc208 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.]. Open Scope nat_scope.
-V7only [Import R_scope.]. Open Scope R_scope.
+V7only [Import nat_scope.]. Open Local Scope nat_scope.
+V7only [Import R_scope.]. Open Local 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 5196cba383..c59c00e089 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 66a66f399d..3f09864806 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -10,7 +10,7 @@
 
 Require RIneq.
 Require Omega.
-V7only [Import R_scope.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 34c9a2c500..175883ba88 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 3f06c65d8e..330d538126 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 5878481a56..961f8bf0ad 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local Scope R_scope.
 
 (*******************************************)
 (*            Newton's Integral            *)
diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v
index 422cbcf6a1..2576d9275f 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 7f6bd91775..9db2ebc660 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 025eb54101..ac61adeb78 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.]. Open Scope nat_scope.
-V7only [Import Z_scope.]. Open Scope Z_scope.
-V7only [Import R_scope.]. Open Scope R_scope.
+V7only [Import nat_scope.]. Open Local Scope nat_scope.
+V7only [Import Z_scope.]. Open Local Scope Z_scope.
+V7only [Import R_scope.]. Open Local Scope R_scope.
 
 Implicit Variable Type r:R.
 
diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v
index 00563ebcd3..3cccc2bfcf 100644
--- a/theories/Reals/RList.v
+++ b/theories/Reals/RList.v
@@ -10,7 +10,7 @@
 
 Require Rbase.
 Require Rfunctions.
-V7only [Import R_scope.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local Scope R_scope.
 
 Inductive Rlist : Type :=
 | nil : Rlist
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
index 44e35a6d97..81baa6c295 100644
--- a/theories/Reals/R_Ifp.v
+++ b/theories/Reals/R_Ifp.v
@@ -16,6 +16,8 @@
 Require Rbase.
 Require Omega.
 
+Open Local Scope R_scope.
+
 (*********************************************************)
 (**      Fractional part                                 *)
 (*********************************************************)
diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v
index f710c5120c..0610db3bea 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local Scope R_scope.
 
 (****************************************************)
 (* Rsqr : some results                              *)
diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v
index c3997a3124..759e4b164a 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 6e144928ed..4f944995c1 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local Scope R_scope.
 
 Axiom AppVar : R.
 
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index aa41a8ae0f..42293730ce 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local Scope R_scope.
 Implicit Variable Type f:R->R.
 
 (****************************************************)
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v
index d13e96668c..70f7adb1fb 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 7137deac3b..e8af542acc 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 4da04bab8a..6db2609a9c 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 3d312634d5..64671d00da 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local Scope R_scope.
 
 (*********************************************************)
 (*               Field axioms                            *)
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 71fa79ad2e..31369adfe3 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local Scope R_scope.
 
 Implicit Variable Type r:R.
 
diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v
index c9f2596aa4..edcddeb25a 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local Scope R_scope.
 
 (****************************************************)
 (*              R is complete :                     *)
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v
index d73c101689..4f74203064 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 b7be1f077f..76752c6450 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local Scope R_scope.
 
 (*******************************)
 (**     Factorial              *)
diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v
index 8168571e86..6e7a3bc671 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 63322838a9..a1f7101eff 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local Scope R_scope.
 
 Implicit Arguments On.
 
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index d436e780f4..d4d25b1120 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local Scope R_scope.
 
 Implicit Arguments On.
 
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index f21ddcef94..6ad02e50c1 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local Scope R_scope.
 
 (*******************************)
 (*      Calculus               *)
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index 0c641c692a..10301bf6e8 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 10dd8eb837..0093eb15e8 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 f0cefb2e89..445343f7af 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local Scope R_scope.
 
 Set Implicit Arguments.
 
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 2f11d30013..94917e42a0 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local Scope R_scope.
 
 Fixpoint Dichotomy_lb [x,y:R;P:R->bool;N:nat] : R :=
 Cases N of 
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index b08ef82724..14cb0c8084 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -235,9 +235,10 @@ Notation "/ x" := (Rinv x) (at level 0): R_scope
   V8only (at level 30, left associativity).
 
 V7only [
-Open Scope R_scope.
+Open Local Scope R_scope.
 End R_scope.
 ].
 
 Delimits Scope R_scope with R.
 
+Arguments Scope up [R_scope].
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v
index c32e76ce2d..c59db60cef 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 c2fbf5d324..c66112d5fe 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 87dbc98b48..7e8ef465bc 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 52a1fa0303..f5e3912bff 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 a2b2ebe058..de7a495681 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local Scope R_scope.
 
 (*****************************)
 (* Definition of exponential *)
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index bc04d7470a..adb1aea4c4 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 a49727b87b..ca232ccb9a 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 d968112c58..088a9280e0 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local 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 859c95753b..35f6d0f32c 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.]. Open Scope R_scope.
+V7only [Import R_scope.]. Open Local Scope R_scope.
 
 (**********)
 Lemma sqrt_var_maj : (h:R) ``(Rabsolu h) <= 1`` -> ``(Rabsolu ((sqrt (1+h))-1))<=(Rabsolu h)``.