diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-22 16:01:53 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-22 16:01:53 +0000 |
| commit | 92e6a939db93015e17c8b6d5b699aaf7e0b3cc9d (patch) | |
| tree | d4c6dd9ae528011c1eb15d12e0c9d5afc3c2ed19 /theories/NArith | |
| parent | f0168fd8ce775b0a96e8cf026e953e9d55f4de25 (diff) | |
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
Diffstat (limited to 'theories/NArith')
| -rw-r--r-- | theories/NArith/BinNat.v | 2 | ||||
| -rw-r--r-- | 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 21aaabcbc..59167545a 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 3e25d8316..750da2397 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 |