From 9beafe7c3fde8adfd3f9afdd74fe6842cceefe32 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 3 May 2005 20:44:01 +0000
Subject: Open Scope non Local malencontreux

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6987 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/omega/OmegaLemmas.v  | 4 ++--
 contrib7/omega/OmegaLemmas.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/contrib/omega/OmegaLemmas.v b/contrib/omega/OmegaLemmas.v
index 298d38959c..294c5a4372 100644
--- a/contrib/omega/OmegaLemmas.v
+++ b/contrib/omega/OmegaLemmas.v
@@ -10,7 +10,7 @@
 
 Require Import ZArith_base.
 
-Open Scope Z_scope.
+Open Local Scope Z_scope.
 
 (** These are specific variants of theorems dedicated for the Omega tactic *)
 
@@ -260,4 +260,4 @@ Definition fast_Zred_factor5 (x y : Z) (P : Z -> Prop)
   (H : P y) := eq_ind_r P H (Zred_factor5 x y).
 
 Definition fast_Zred_factor6 (x : Z) (P : Z -> Prop) 
-  (H : P (x + 0)) := eq_ind_r P H (Zred_factor6 x).
\ No newline at end of file
+  (H : P (x + 0)) := eq_ind_r P H (Zred_factor6 x).
diff --git a/contrib7/omega/OmegaLemmas.v b/contrib7/omega/OmegaLemmas.v
index b27afd0dd8..a75577e314 100644
--- a/contrib7/omega/OmegaLemmas.v
+++ b/contrib7/omega/OmegaLemmas.v
@@ -10,7 +10,7 @@
 
 Require ZArith_base.
 
-Open Scope Z_scope.
+Open Local Scope Z_scope.
 
 (** These are specific variants of theorems dedicated for the Omega tactic *)
 
-- 
cgit v1.2.3