From 92e6a939db93015e17c8b6d5b699aaf7e0b3cc9d Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 22 Oct 2010 16:01:53 +0000
Subject: Still another Open Scope than should be Local

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

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 21aaabcbc7..59167545ad 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -25,7 +25,7 @@ Delimit Scope N_scope with N.
 Bind Scope N_scope with N.
 Arguments Scope Npos [positive_scope].
 
-Open Local Scope N_scope.
+Local Open Scope N_scope.
 
 Definition Ndiscr : forall n:N, { p:positive | n = Npos p } + { n = N0 }.
 Proof.
diff --git a/theories/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v
index 3e25d83162..750da23976 100644
--- a/theories/NArith/Nsqrt_def.v
+++ b/theories/NArith/Nsqrt_def.v
@@ -10,7 +10,7 @@
 
 Require Import BinPos BinNat Psqrt.
 
-Open Scope N_scope.
+Local Open Scope N_scope.
 
 Definition Nsqrtrem n :=
  match n with
-- 
cgit v1.2.3