diff options
Diffstat (limited to 'theories/Numbers/NatInt')
| -rw-r--r-- | theories/Numbers/NatInt/NZDomain.v | 4 |
1 files changed, 3 insertions, 1 deletions
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. |