diff options
Diffstat (limited to 'theories/Numbers/Integer/NatPairs/ZNatPairs.v')
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZNatPairs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 3f5583927a..facffef45f 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -96,7 +96,7 @@ Notation Local plus_wd := NZplus_wd (only parsing). Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. Module Export NZAxiomsMod <: NZAxiomsSig. -Definition NZ : Set := Z. +Definition NZ : Type := Z. Definition NZeq := Zeq. Definition NZ0 := Z0. Definition NZsucc := Zsucc. |