From 120ed3238345fb088afbfa5dac153dc28e4bc6ee Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 9 Apr 2003 16:24:49 +0000
Subject: Ajout Open Scope

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3890 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/ZArith/Wf_Z.v         | 1 +
 theories/ZArith/ZArith_dec.v   | 2 +-
 theories/ZArith/Zcomplements.v | 1 +
 theories/ZArith/Zdiv.v         | 1 +
 theories/ZArith/Zlogarithm.v   | 1 +
 theories/ZArith/Zmisc.v        | 1 +
 theories/ZArith/Zpower.v       | 1 +
 theories/ZArith/Zsqrt.v        | 1 +
 theories/ZArith/Zwf.v          | 1 +
 9 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index d02c46e082..035e16f220 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 98c1dc32f9..88e7c325d7 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 34971439b3..954347d89d 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 ce1bd0335b..e888d87d03 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 aa97d4bf87..0fe380e718 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 3e2d8a4aae..8a7a1caa44 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 4dbfa8fc8a..8f695a166f 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 681dcdd122..3c895d6dba 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 569be3b313..5468f82cc8 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. *)
 
-- 
cgit v1.2.3