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
---
 contrib7/omega/OmegaLemmas.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib7')

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