Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".

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

71 files changed, 100 insertions, 75 deletions

diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 5711a81a74..20d5e3f7e1 100755
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -10,7 +10,9 @@
 
 Require Le.
 Require Lt.
-Import nat_scope.
+
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
 
 Section Between.
 Variables P,Q : nat -> Prop.
diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v
index ff7f0ab5ce..f9f6eeb19b 100644
--- a/theories/Arith/Bool_nat.v
+++ b/theories/Arith/Bool_nat.v
@@ -11,7 +11,9 @@
 Require Export Compare_dec.
 Require Export Peano_dec.
 Require Sumbool.
-Import nat_scope.
+
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,x,y:nat.
 
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index 5d7f1e42c9..88055f11e9 100755
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -9,7 +9,8 @@
 (*i $Id$ i*)
 
 (** Equality is decidable on [nat] *)
-Import nat_scope.
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
 
 (*
 Lemma not_eq_sym : (A:Set)(p,q:A)(~p=q) -> ~(q=p).
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index c30b90fae7..1518727e45 100755
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -12,7 +12,9 @@ Require Le.
 Require Lt.
 Require Gt.
 Require Decidable.
-Import nat_scope.
+
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,x,y:nat.
 
diff --git a/theories/Arith/Div.v b/theories/Arith/Div.v
index ed41c5a931..c22235d108 100755
--- a/theories/Arith/Div.v
+++ b/theories/Arith/Div.v
@@ -9,7 +9,9 @@
 (*i $Id$ i*)
 
 (** Euclidean division *)
-Import nat_scope.
+
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
 
 Require Le.
 Require Euclid_def.
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index b05eaa77d8..9ab8fc820e 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -12,7 +12,9 @@ Require Lt.
 Require Plus.
 Require Compare_dec.
 Require Even.
-Import nat_scope.
+
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
 
 Implicit Variables Type n:nat.
 
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index c42deebd26..9b1bca7c45 100755
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -10,7 +10,8 @@
 
 (** Equality on natural numbers *)
 
-Import nat_scope.
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,x,y:nat.
 
diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v
index 7f4e325be0..f64d932e76 100644
--- a/theories/Arith/Euclid.v
+++ b/theories/Arith/Euclid.v
@@ -11,7 +11,9 @@
 Require Mult.
 Require Compare_dec.
 Require Wf_nat.
-Import nat_scope.
+
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
 
 Implicit Variables Type a,b,n,q,r:nat.
 
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index ca0637955c..8b3c7b563b 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -12,7 +12,7 @@
     and we prove the decidability and the exclusion of those predicates.
     The main results about parity are proved in the module Div2. *)
 
-Import nat_scope.
+V7only [Import nat_scope.].
 
 Implicit Variables Type m,n:nat.
 
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index d4bc8531db..b730e9d7fb 100755
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -11,7 +11,8 @@
 Require Le.
 Require Lt.
 Require Plus.
-Import nat_scope.
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,p:nat.
 
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index 5321637bea..3aec6ec3a7 100755
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -9,8 +9,8 @@
 (*i $Id$ i*)
 
 (** Order on natural numbers *)
-Import nat_scope.
-Open Scope nat_scope.
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,p:nat.
 
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 94bb00c8f8..beb32fac81 100755
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -9,7 +9,8 @@
 (*i $Id$ i*)
 
 Require Le.
-Import nat_scope.
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,p:nat.
 
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 8b4c86cd53..ac8ff97a19 100755
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -10,7 +10,8 @@
 
 Require Arith.
 
-Import nat_scope.
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
 
 Implicit Variables Type m,n:nat.
 
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index a762a06d56..81559526bd 100755
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -10,7 +10,8 @@
 
 Require Arith.
 
-Import nat_scope.
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
 
 Implicit Variables Type m,n:nat.
 
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index de06c097af..2d00f259b4 100755
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -12,7 +12,9 @@
 
 Require Lt.
 Require Le.
-Import nat_scope.
+
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,p:nat.
 
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 7c2ea25cd4..da1fbe02c3 100755
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -11,7 +11,9 @@
 Require Export Plus.
 Require Export Minus.
 Require Export Lt.
-Import nat_scope.
+
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,p:nat.
 
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index c5f0ecdcc8..96a8523f9f 100755
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -10,7 +10,8 @@
 
 Require Decidable.
 
-Import nat_scope.
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,x,y:nat.
 
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index debad4ca71..2285c544cd 100755
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -13,7 +13,8 @@
 Require Le.
 Require Lt.
 
-Import nat_scope.
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,p,q:nat.
 
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 0c299bd371..ef292d4c12 100755
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -12,7 +12,8 @@
 
 Require Lt.
 
-Import nat_scope.
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,p:nat.
 
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v
index e86a4d0037..36131beb0a 100644
--- a/theories/Reals/Alembert.v
+++ b/theories/Reals/Alembert.v
@@ -14,7 +14,7 @@ Require Rseries.
 Require SeqProp.
 Require PartSum.
 Require Max.
-Import R_scope.
+V7only [Import R_scope.].
 
 (***************************************************)
 (* Various versions of the criterion of D'Alembert *)
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index 5c7f02d4df..7047bb03dd 100644
--- a/theories/Reals/AltSeries.v
+++ b/theories/Reals/AltSeries.v
@@ -14,7 +14,7 @@ Require Rseries.
 Require SeqProp.
 Require PartSum.
 Require Max.
-Import R_scope.
+V7only [Import 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 18e833e692..62d1609343 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -12,7 +12,7 @@ Require Rbase.
 Require Rbasic_fun.
 Require Even.
 Require Div2.
-Import R_scope.
+V7only [Import 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 c97f98474d..03b6b46fcd 100644
--- a/theories/Reals/Binomial.v
+++ b/theories/Reals/Binomial.v
@@ -11,7 +11,7 @@
 Require Rbase.
 Require Rfunctions.
 Require PartSum.
-Import R_scope.
+V7only [Import 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 c6926ec189..5cd8bf6721 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.
-Import R_scope.
+V7only [Import 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 e366adb384..ae650225f2 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.
-Import nat_scope.
-Import R_scope.
+V7only [Import nat_scope.].
+V7only [Import 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 fb41d99276..b773057ed8 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.
-Import R_scope.
+V7only [Import 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 791954d063..62bf0265d2 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -10,7 +10,7 @@
 
 Require RIneq.
 Require Omega.
-Import R_scope.
+V7only [Import 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 8a16bfdf11..ca5de937be 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.
-Import R_scope.
+V7only [Import 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 3e2ff2bb7d..7de5c64c02 100644
--- a/theories/Reals/MVT.v
+++ b/theories/Reals/MVT.v
@@ -12,7 +12,7 @@ Require Rbase.
 Require Rfunctions.
 Require Ranalysis1.
 Require Rtopology.
-Import R_scope.
+V7only [Import 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 8f7a4fa11e..7c7cb59ea2 100644
--- a/theories/Reals/NewtonInt.v
+++ b/theories/Reals/NewtonInt.v
@@ -13,7 +13,7 @@ Require Rfunctions.
 Require SeqSeries.
 Require Rtrigo.
 Require Ranalysis.
-Import R_scope.
+V7only [Import R_scope.].
 
 (*******************************************)
 (*            Newton's Integral            *)
diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v
index 92549a55e0..8a4aa1fc5f 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.
-Import R_scope.
+V7only [Import 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 0b3da1ea71..66d3496d3b 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -13,7 +13,7 @@ Require Rfunctions.
 Require Rseries.
 Require Rcomplete.
 Require Max.
-Import R_scope.
+V7only [Import 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 a09ec91742..0f57c281d4 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.
-Import nat_scope.
-Import Z_scope.
-Import R_scope.
+V7only [Import nat_scope.].
+V7only [Import Z_scope.].
+V7only [Import R_scope.].
 
 Implicit Variable Type r:R.
 
diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v
index ce022d7c14..edfb48728d 100644
--- a/theories/Reals/RList.v
+++ b/theories/Reals/RList.v
@@ -10,7 +10,7 @@
 
 Require Rbase.
 Require Rfunctions.
-Import R_scope.
+V7only [Import R_scope.].
 
 Inductive Rlist : Type :=
 | nil : Rlist
diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v
index 9e8b81d3ee..2fa84607fb 100644
--- a/theories/Reals/R_sqr.v
+++ b/theories/Reals/R_sqr.v
@@ -10,7 +10,7 @@
 
 Require Rbase.
 Require Rbasic_fun.
-Import R_scope.
+V7only [Import R_scope.].
 
 (****************************************************)
 (* Rsqr : some results                              *)
diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v
index 01f0662a9d..0fd4192882 100644
--- a/theories/Reals/R_sqrt.v
+++ b/theories/Reals/R_sqrt.v
@@ -11,7 +11,7 @@
 Require Rbase.
 Require Rfunctions.
 Require Rsqrt_def.
-Import R_scope.
+V7only [Import 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 40d484dcd4..d467261c72 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.
-Import R_scope.
+V7only [Import R_scope.].
 
 Axiom AppVar : R.
 
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v
index e2bc87ffe2..05cfabcba8 100644
--- a/theories/Reals/Ranalysis2.v
+++ b/theories/Reals/Ranalysis2.v
@@ -11,7 +11,7 @@
 Require Rbase.
 Require Rfunctions.
 Require Ranalysis1.
-Import R_scope.
+V7only [Import 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 0ccda909d0..35f28aa64d 100644
--- a/theories/Reals/Ranalysis3.v
+++ b/theories/Reals/Ranalysis3.v
@@ -12,7 +12,7 @@ Require Rbase.
 Require Rfunctions.
 Require Ranalysis1.
 Require Ranalysis2.
-Import R_scope.
+V7only [Import 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 5dc3991e24..23c52c330e 100644
--- a/theories/Reals/Ranalysis4.v
+++ b/theories/Reals/Ranalysis4.v
@@ -15,7 +15,7 @@ Require Rtrigo.
 Require Ranalysis1.
 Require Ranalysis3.
 Require Exp_prop.
-Import R_scope.
+V7only [Import 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 4555116334..6775958fcc 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.
-Import R_scope.
+V7only [Import R_scope.].
 
 (*********************************************************)
 (*               Field axioms                            *)
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 57de5d5b92..0c173c9512 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -16,7 +16,7 @@
 Require Rbase.
 Require R_Ifp.
 Require Fourier.
-Import R_scope.
+V7only [Import R_scope.].
 
 Implicit Variable Type r:R.
 
diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v
index 151f2b2639..e62db41e5a 100644
--- a/theories/Reals/Rcomplete.v
+++ b/theories/Reals/Rcomplete.v
@@ -13,7 +13,7 @@ Require Rfunctions.
 Require Rseries.
 Require SeqProp.
 Require Max.
-Import R_scope.
+V7only [Import R_scope.].
 
 (****************************************************)
 (*              R is complete :                     *)
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v
index b5c0c6b1c3..392c299a07 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.
-Import R_scope.
+V7only [Import 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 e4cfa330ab..1131f11678 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.
-Import R_scope.
+V7only [Import R_scope.].
 
 (*******************************)
 (**     Factorial              *)
diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v
index b36b9ad355..831b32b9ed 100644
--- a/theories/Reals/Rgeom.v
+++ b/theories/Reals/Rgeom.v
@@ -13,7 +13,7 @@ Require Rfunctions.
 Require SeqSeries.
 Require Rtrigo.
 Require R_sqrt.
-Import R_scope.
+V7only [Import 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 7966d9c88b..55869a1100 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.
-Import R_scope.
+V7only [Import R_scope.].
 
 Implicit Arguments On.
 
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index 8c1329e4ed..46157e3c9e 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.
-Import R_scope.
+V7only [Import R_scope.].
 
 Implicit Arguments On.
 
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index c9ad0032d9..7f2baa8efa 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -17,7 +17,7 @@ Require Rbase.
 Require Rfunctions.
 Require Classical_Prop.
 Require Fourier.
-Import R_scope.
+V7only [Import R_scope.].
 
 (*******************************)
 (*      Calculus               *)
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index 096ab1eaa8..e76236a894 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.
-Import R_scope.
+V7only [Import 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 7089ac26c8..24eba0cefe 100644
--- a/theories/Reals/Rprod.v
+++ b/theories/Reals/Rprod.v
@@ -14,7 +14,7 @@ Require Rfunctions.
 Require Rseries.
 Require PartSum.
 Require Binomial.
-Import R_scope.
+V7only [Import 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 21cf09264c..4769c0cd26 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.v
@@ -12,7 +12,7 @@ Require Rbase.
 Require Rfunctions.
 Require Rseries.
 Require PartSum.
-Import R_scope.
+V7only [Import R_scope.].
 
 Set Implicit Arguments.
 
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 6496c99823..8267692a6d 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.
-Import R_scope.
+V7only [Import 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 4624850e90..5dc510c66d 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.
-Import R_scope.
+V7only [Import 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 f265b4a772..28a9fccb83 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.
-Import R_scope.
+V7only [Import 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 d147d68ac4..1f8b0ad079 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.
-Import R_scope.
+V7only [Import R_scope.].
 
 (*****************************************************************)
 (* Using series definitions of cos and sin                       *)
diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v
index cfa65824bf..925d7be950 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.
-Import R_scope.
+V7only [Import 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 cf2ba3dd2f..8ede5a7a13 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.
-Import R_scope.
+V7only [Import R_scope.].
 
 (*****************************)
 (* Definition of exponential *)
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index aa1c2b9d75..6ec18e56a2 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.
-Import R_scope.
+V7only [Import 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 e64d9cc4f7..3f1a84f9de 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -13,7 +13,7 @@ Require Rfunctions.
 Require Rseries.
 Require Classical.
 Require Max.
-Import R_scope.
+V7only [Import 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 14d4380773..f3cc24ae91 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.
-Import R_scope.
+V7only [Import 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 ccda09a0b4..7d282e5921 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.
-Import R_scope.
+V7only [Import R_scope.].
 
 (**********)
 Lemma sqrt_var_maj : (h:R) ``(Rabsolu h) <= 1`` -> ``(Rabsolu ((sqrt (1+h))-1))<=(Rabsolu h)``.
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index cd74d0bad6..d02c46e082 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -12,7 +12,7 @@ Require fast_integer.
 Require zarith_aux.
 Require auxiliary.
 Require Zsyntax.
-Import Z_scope.
+V7only [Import Z_scope.].
 
 (** Our purpose is to write an induction shema for {0,1,2,...}
   similar to the [nat] schema (Theorem [Natlike_rec]). For that the
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index 7037a5cacd..98c1dc32f9 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -14,7 +14,7 @@ Require fast_integer.
 Require zarith_aux.
 Require auxiliary.
 Require Zsyntax.
-Import Z_scope.
+V7only [Import Z_scope.].
 
 
 Lemma Dcompare_inf : (r:relation) {r=EGAL} + {r=INFERIEUR} + {r=SUPERIEUR}.
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index ccbad9de2c..34971439b3 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -12,7 +12,7 @@ Require ZArith_base.
 Require ZArithRing.
 Require Omega.
 Require Wf_nat.
-Import Z_scope.
+V7only [Import Z_scope.].
 
 (** Multiplication by a number >0 preserves [Zcompare]. It also perserves
     [Zle], [Zlt], [Zge], [Zgt] *)
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index f3cf93e0c1..ce1bd0335b 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -23,7 +23,7 @@ Require Export ZArith_base.
 Require Omega.
 Require ZArithRing.
 Require Zcomplements.
-Import Z_scope.
+V7only [Import Z_scope.].
 
 (**
 
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v
index 52e2f552e4..aa97d4bf87 100644
--- a/theories/ZArith/Zlogarithm.v
+++ b/theories/ZArith/Zlogarithm.v
@@ -23,7 +23,7 @@ Require ZArith_base.
 Require Omega.
 Require Zcomplements.
 Require Zpower.
-Import Z_scope.
+V7only [Import Z_scope.].
 
 Section Log_pos. (* Log of positive integers *)
 
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index 2ed6386960..3e2d8a4aae 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -13,7 +13,7 @@ Require zarith_aux.
 Require auxiliary.
 Require Zsyntax.
 Require Bool.
-Import Z_scope.
+V7only [Import Z_scope.].
 
 (** Overview of the sections of this file:
     - logic: Logic complements.
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 8b68b223d5..4dbfa8fc8a 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -11,7 +11,7 @@
 Require ZArith_base.
 Require Omega.
 Require Zcomplements.
-Import Z_scope.
+V7only [Import Z_scope.].
 
 Section section1.
 
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index a5ddfff4f1..681dcdd122 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -11,7 +11,7 @@
 Require Export ZArith_base.
 Require Export ZArithRing.
 Require Export Omega.
-Import Z_scope.
+V7only [Import Z_scope.].
 
 (** The following tactic replaces all instances of (POS (xI ...)) by
     `2*(POS ...)+1` , but only when ... is not made only with xO, XI, or xH. *)
diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v
index d93a6ea443..569be3b313 100644
--- a/theories/ZArith/Zwf.v
+++ b/theories/ZArith/Zwf.v
@@ -11,7 +11,7 @@
 Require ZArith_base.
 Require Export Wf_nat.
 Require Omega.
-Import Z_scope.
+V7only [Import Z_scope.].
 
 (** Well-founded relations on Z. *)