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

9 files changed, 9 insertions, 9 deletions

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. *)