Use OCaml floating-point operations on 64 bits arch

C functions were used for floating-point arithmetic operations, by
fear of double rounding that could happen on old x87 on 32 bits
architecture. This commit uses OCaml floating-point operations on 64
bits architectures.

The following snippet is made 17% faster by this commit.

    From Coq Require Import Int63 BinPos PrimFloat.
    Definition foo n :=
      let eps := sub (next_up one) one in
      Pos.iter (fun x => add x eps) two n.
    Time Eval native_compute in foo 1000000000.

0 files changed, 0 insertions, 0 deletions