diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-22 11:08:13 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-22 11:08:13 +0000 |
| commit | cf73432c0e850242c7918cc348388e5cde379a8f (patch) | |
| tree | 07ebc5fa4588f13416caaca476f90816beb867ae /theories/Numbers/Integer/NatPairs | |
| parent | 313de91c9cd26e6fee94aa5bb093ae8a436fd43a (diff) | |
switch theories/Numbers from Set to Type (both the abstract and the bignum part).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10964 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer/NatPairs')
| -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 3f5583927..facffef45 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. |