aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rwxr-xr-xtheories/Bool/Bool.v2
-rw-r--r--theories/ZArith/fast_integer.v2
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 *)