diff options
| -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 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 |