diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-27 14:22:37 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-27 14:22:37 +0000 |
| commit | aabccf49938d5727cc1c7a53882ce1f5108bbed5 (patch) | |
| tree | 091945168595d81915b695e68a690352b22a6b22 /theories/ZArith/Zmisc.v | |
| parent | dd866fe3894d3d7542b45fb881aa2280378b2ae4 (diff) | |
Some more cleanups (Zeven, auxiliary, Zbool, Zmisc, ZArith_base)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14241 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zmisc.v')
| -rw-r--r-- | theories/ZArith/Zmisc.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index 6f512e4f3..ff844ec28 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -21,8 +21,8 @@ Open Local Scope Z_scope. Notation iter := @Z.iter (only parsing). Lemma iter_nat_of_Z : forall n A f x, 0 <= n -> - iter n A f x = iter_nat (Zabs_nat n) A f x. + iter n A f x = iter_nat (Z.abs_nat n) A f x. intros n A f x; case n; auto. -intros p _; unfold Z.iter, Zabs_nat; apply iter_nat_of_P. +intros p _; unfold Z.iter, Z.abs_nat; apply iter_nat_of_P. intros p abs; case abs; trivial. Qed. |