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

1 files changed, 3 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index c7e5b30d75..694d17f352 100644
--- a/CHANGES
+++ b/CHANGES
@@ -25,7 +25,9 @@ Libraries
 - Important revision of NArith and ZArith. In particular some definitions
   or lemmas may have moved. The alternative division (Trunc convention
   instead of Floor) is now named Zquot (noted ÷) and Zrem by analogy
-  with Haskell. TODO: say more later.
+  with Haskell. In Zeven, the behavior of Zdiv2 on negative numbers has been
+  changed to be consistent with Zdiv, while the old behavior now corresponds
+  to function Zquot2. TODO: say more later.
 - When creating BigN, the macro-generated part NMake_gen is much smaller.
   The generic part NMake has been reworked and improved. Some changes
   may introduce incompatibilities. In particular, the order of the arguments