From f87c74e95b89d61cc739bde85b95b3e5055d9b96 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 26 Sep 2003 11:33:55 +0000
Subject: 'Open Local Scope' en attendant que le core_scope sache se mettre
 devant implicitement

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4485 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Bool/Bool.v           | 2 +-
 theories/ZArith/fast_integer.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 8da809d500..0e254c8e59 100755
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -178,7 +178,7 @@ Infix "&&" andb (at level 3, no associativity) : bool_scope
 Notation "- b" := (negb b) (at level 0, right associativity) : bool_scope
   V8only.
 
-Open Scope bool_scope.
+Open Local Scope bool_scope.
 
 (**************************)
 (** Lemmas about [negb]   *)
diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v
index 26a5a738e2..7b4e26c033 100644
--- a/theories/ZArith/fast_integer.v
+++ b/theories/ZArith/fast_integer.v
@@ -1313,7 +1313,7 @@ Definition Zcompare := [x,y:Z]
 
 V8Infix "?=" Zcompare (at level 50, no associativity) : Z_scope.
 
-Open Scope Z_scope.
+Open Local Scope Z_scope.
 
 (**********************************************************************)
 (** Properties of opposite on binary integer numbers *)
-- 
cgit v1.2.3