From 46ab3659dd1f2e4839064cfabc03bd19268fa44b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 30 Mar 2018 14:47:06 +0200
Subject: Adapting standard library to the introduction of "Declare Scope".

Removing in passing two Local which are no-ops in practice.
---
 theories/Numbers/NatInt/NZDomain.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'theories/Numbers/NatInt')

diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index 3d0c005fd1..acebfcf1d2 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -220,8 +220,10 @@ End NZDomainProp.
 Module NZOfNat (Import NZ:NZDomainSig').
 
 Definition ofnat (n : nat) : t := (S^n) 0.
-Notation "[ n ]" := (ofnat n) (at level 7) : ofnat.
+
+Declare Scope ofnat.
 Local Open Scope ofnat.
+Notation "[ n ]" := (ofnat n) (at level 7) : ofnat.
 
 Lemma ofnat_zero : [O] == 0.
 Proof.
-- 
cgit v1.2.3