From 9ff6f3029e0a275d8630f055bdb78e2c15e8bb29 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 12 Feb 2006 22:08:04 +0000
Subject: Bug Scope

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8034 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/ZArith/Zminmax.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v
index c311c7ce9d..a862c56193 100644
--- a/theories/ZArith/Zminmax.v
+++ b/theories/ZArith/Zminmax.v
@@ -10,7 +10,7 @@
 Require Import Zmin Zmax.
 Require Import BinInt Zorder.
 
-Open Scope Z_scope.
+Open Local Scope Z_scope.
 
 (** *** Lattice properties of min and max on Z *)
 
-- 
cgit v1.2.3