Numbers and bitwise functions.

 See NatInt/NZBits.v for the common axiomatization of bitwise functions
 over naturals / integers. Some specs aren't pretty, but easier to
 prove, see alternate statements in property functors {N,Z}Bits.
 Negative numbers are considered via the two's complement convention.

 We provide implementations for N (in Ndigits.v), for nat (quite dummy,
 just for completeness), for Z (new file Zdigits_def), for BigN
 (for the moment partly by converting to N, to be improved soon)
 and for BigZ.

 NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in
 the reversed order (for consistency with the rest of the world):
 for instance BigN.shiftl 1 10 is 2^10.

 NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2)
 on negative numbers. For the moment I've kept it intact, and have
 just added a Zdiv2' which is truly equivalent to (Zdiv _ 2).
 To reorganize someday ?

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13689 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 07b8dfea4e..c7e5b30d75 100644
--- a/CHANGES
+++ b/CHANGES
@@ -26,8 +26,11 @@ Libraries
   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.
-- When creating BigN, the macro-generated part NMake_gen is much smaller,
-  improvements of the generic part NMake.
+- 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
+  for BigN.shiftl and BigN.shiftr is now reversed: the number to shift now
+  comes first. By default, the power function now takes two BigN.
 
 Internal infrastructure