sig
  type 'a bvector = int64
  exception Overflow
  val xO : 'a CoqBvector.bvector -> 'a CoqBvector.bvector
  val xI : 'a CoqBvector.bvector -> 'a CoqBvector.bvector
  val plus :
    'a CoqBvector.bvector -> 'a CoqBvector.bvector -> 'a CoqBvector.bvector
  val minus :
    'a CoqBvector.bvector -> 'a CoqBvector.bvector -> 'a CoqBvector.bvector
  val times :
    'a CoqBvector.bvector -> 'a CoqBvector.bvector -> 'a CoqBvector.bvector
  val inc : CoqNat.nat -> 'a CoqBvector.bvector -> 'a CoqBvector.bvector
  val dec : CoqNat.nat -> 'a CoqBvector.bvector -> 'a CoqBvector.bvector
  val bvec_to_nat : CoqNat.nat -> 'a CoqBvector.bvector -> CoqNat.nat
  val nat_to_bvec : CoqNat.nat -> CoqNat.nat -> 'a CoqBvector.bvector
  val bvec_eq_dec :
    CoqNat.nat -> 'a CoqBvector.bvector -> 'a CoqBvector.bvector -> bool
  val bneg : CoqNat.nat -> 'a CoqBvector.bvector -> 'a CoqBvector.bvector
  val bVand :
    CoqNat.nat ->
    'a CoqBvector.bvector -> 'a CoqBvector.bvector -> 'a CoqBvector.bvector
  val bVor :
    CoqNat.nat ->
    'a CoqBvector.bvector -> 'a CoqBvector.bvector -> 'a CoqBvector.bvector
end