diff options
| author | letouzey | 2008-05-22 11:08:13 +0000 |
|---|---|---|
| committer | letouzey | 2008-05-22 11:08:13 +0000 |
| commit | cf73432c0e850242c7918cc348388e5cde379a8f (patch) | |
| tree | 07ebc5fa4588f13416caaca476f90816beb867ae /theories/Numbers/Integer | |
| 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')
| -rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZNatPairs.v | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 5927c2beab..83171388d9 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -17,7 +17,7 @@ Open Scope Z_scope. Module Type NType. - Parameter t : Set. + Parameter t : Type. Parameter zero : t. Parameter one : t. @@ -101,7 +101,7 @@ End NType. Module Make (N:NType). - Inductive t_ : Set := + Inductive t_ := | Pos : N.t -> t_ | Neg : N.t -> t_. 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. |