Ajout Open Scope

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

9 files changed, 9 insertions, 1 deletions

diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index d02c46e08..035e16f22 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -13,6 +13,7 @@ Require zarith_aux.
 Require auxiliary.
 Require Zsyntax.
 V7only [Import Z_scope.].
+Open Local Scope 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 98c1dc32f..88e7c325d 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -15,7 +15,7 @@ Require zarith_aux.
 Require auxiliary.
 Require Zsyntax.
 V7only [Import Z_scope.].
-
+Open Local Scope Z_scope.
 
 Lemma Dcompare_inf : (r:relation) {r=EGAL} + {r=INFERIEUR} + {r=SUPERIEUR}.
 Proof.
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 34971439b..954347d89 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -13,6 +13,7 @@ Require ZArithRing.
 Require Omega.
 Require Wf_nat.
 V7only [Import Z_scope.].
+Open Local Scope 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 ce1bd0335..e888d87d0 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -24,6 +24,7 @@ Require Omega.
 Require ZArithRing.
 Require Zcomplements.
 V7only [Import Z_scope.].
+Open Local Scope Z_scope.
 
 (**
 
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v
index aa97d4bf8..0fe380e71 100644
--- a/theories/ZArith/Zlogarithm.v
+++ b/theories/ZArith/Zlogarithm.v
@@ -24,6 +24,7 @@ Require Omega.
 Require Zcomplements.
 Require Zpower.
 V7only [Import Z_scope.].
+Open Local Scope Z_scope.
 
 Section Log_pos. (* Log of positive integers *)
 
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index 3e2d8a4aa..8a7a1caa4 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -14,6 +14,7 @@ Require auxiliary.
 Require Zsyntax.
 Require Bool.
 V7only [Import Z_scope.].
+Open Local Scope 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 4dbfa8fc8..8f695a166 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -12,6 +12,7 @@ Require ZArith_base.
 Require Omega.
 Require Zcomplements.
 V7only [Import Z_scope.].
+Open Local Scope Z_scope.
 
 Section section1.
 
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index 681dcdd12..3c895d6db 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -12,6 +12,7 @@ Require Export ZArith_base.
 Require Export ZArithRing.
 Require Export Omega.
 V7only [Import Z_scope.].
+Open Local Scope 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 569be3b31..5468f82cc 100644
--- a/theories/ZArith/Zwf.v
+++ b/theories/ZArith/Zwf.v
@@ -12,6 +12,7 @@ Require ZArith_base.
 Require Export Wf_nat.
 Require Omega.
 V7only [Import Z_scope.].
+Open Local Scope Z_scope.
 
 (** Well-founded relations on Z. *)