diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-09 14:15:19 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-09 14:15:19 +0000 |
| commit | 7c95ca8997a3b561679fc90995d608dbb1da996e (patch) | |
| tree | 562e41df4be2b93323bdfc638bf9ea0eaf6e7d28 /theories/ZArith/Zdigits.v | |
| parent | 76b901471bfdc69a9e0af1300dd4bcaad1e0a17c (diff) | |
ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2
Now we have:
- Zdiv and Zdiv2 : round toward bottom, no easy sign rule, remainder
of a/2 is 0 or 1, operations related with two's-complement Zshiftr.
- Zquot and Zquot2 : round toward zero, Zquot2 (-a) = - Zquot2 a,
remainder of a/2 is 0 or Zsgn a.
Ok, I'm introducing an incompatibility here, but I think coherence is
really desirable. Anyway, people using Zdiv on positive numbers only
shouldn't even notice the change. Otherwise, it's just a matter of
sed -e "s/div2/quot2/g".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13695 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zdigits.v')
| -rw-r--r-- | theories/ZArith/Zdigits.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v index 1bea2bbbe..6d8a237e5 100644 --- a/theories/ZArith/Zdigits.v +++ b/theories/ZArith/Zdigits.v @@ -219,7 +219,7 @@ Section Z_BRIC_A_BRAC. destruct (Zeven.Zeven_odd_dec z); intros. rewrite <- Zeven.Zeven_div2; auto. - generalize (Zeven.Zodd_div2 z H z0); omega. + generalize (Zeven.Zodd_div2 z z0); omega. Qed. Lemma Z_to_two_compl_Sn_z : |