Skip to content
  • Xavier Leroy's avatar
    Move Z definitions out of Integers and into Zbits · 08fd5faf
    Xavier Leroy authored
    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.
    08fd5faf