Move Z definitions out of Integers and into Zbits

The module Integers.Make contained lots of definitions and theorems
about Z integers that were independent of the word size.  These
definitions and theorems are useful outside Integers.Make, but
it felt unnatural to fetch them from modules Int or Int64.

This commit moves the word-size-independent definitions and theorems
to a new module, lib/Zbits.v, and fixes their uses in the code base.

1 files changed, 1 insertions, 1 deletions

diff --git a/Makefile b/Makefile
index 5a9701aa..7b1d3a76 100644
--- a/Makefile
+++ b/Makefile
@@ -53,7 +53,7 @@ FLOCQ=\
 # General-purpose libraries (in lib/)
 
 VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \
-  Iteration.v Integers.v Archi.v Fappli_IEEE_extra.v Floats.v \
+  Iteration.v Zbits.v Integers.v Archi.v Fappli_IEEE_extra.v Floats.v \
   Parmov.v UnionFind.v Wfsimpl.v \
   Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v