9 files changed, 9 insertions, 9 deletions
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index cd74d0bad..d02c46e08 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 7037a5cac..98c1dc32f 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 ccbad9de2..34971439b 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 f3cf93e0c..ce1bd0335 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 52e2f552e..aa97d4bf8 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 2ed638696..3e2d8a4aa 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 8b68b223d..4dbfa8fc8 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 a5ddfff4f..681dcdd12 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 d93a6ea44..569be3b31 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. *)