diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-24 23:34:35 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-24 23:34:35 +0000 |
| commit | ea484db49c183ab900a78204e4bb7ec233578bff (patch) | |
| tree | 1afaf038a05f2fdbfb7b01035d9ee161f6cab976 /theories/Reals/RiemannInt_SF.v | |
| parent | 2c5cf7f65af7a76c313475853ca3d6ea8c494a96 (diff) | |
"INZ" déplacé en V8 dans ZArith, juste syntaxique en V7 dans Reals
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4074 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/RiemannInt_SF.v')
| -rw-r--r-- | theories/Reals/RiemannInt_SF.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index d4d25b112..1fc9811e5 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -23,7 +23,7 @@ Implicit Arguments On. Definition Nbound [I:nat->Prop] : Prop := (EX n:nat | (i:nat)(I i)->(le i n)). Lemma IZN_var:(z:Z)(`0<=z`)->{ n:nat | z=(INZ n)}. -Unfold INZ;Intros; Apply inject_nat_complete_inf; Assumption. +Intros; Apply inject_nat_complete_inf; Assumption. Qed. Lemma Nzorn : (I:nat->Prop) (EX n:nat | (I n)) -> (Nbound I) -> (sigTT ? [n:nat](I n)/\(i:nat)(I i)->(le i n)). |