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/NatInt | |
| 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/NatInt')
| -rw-r--r-- | theories/Numbers/NatInt/NZAxioms.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index 0d3b251f39..ef19069955 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -14,7 +14,7 @@ Require Export NumPrelude. Module Type NZAxiomsSig. -Parameter Inline NZ : Set. +Parameter Inline NZ : Type. Parameter Inline NZeq : NZ -> NZ -> Prop. Parameter Inline NZ0 : NZ. Parameter Inline NZsucc : NZ -> NZ. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index b11b840928..f76fa94808 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -370,7 +370,7 @@ Qed. safely removed *) Definition NZsucc_iter (n : nat) (m : NZ) := - nat_rec (fun _ => NZ) m (fun _ l => S l) n. + nat_rect (fun _ => NZ) m (fun _ l => S l) n. Theorem NZlt_succ_iter_r : forall (n : nat) (m : NZ), m < NZsucc_iter (Datatypes.S n) m. |