Inline the functions from coq_float64.h.

Since the code is compiled in -fPIC mode, the compiler cannot inline the
functions, due to the ABI mandating the ability to interpose visible
symbols. Hiding the symbols of coq_float64.h would work, except that they
float64.ml needs to reference them. (See #13124 for more details.)

This commit improves performances by 7% on the following code.

    From Coq Require Import Int63 BinPos PrimFloat.
    Definition foo n :=
      let two := of_int63 2 in
      Pos.iter (fun x => sub (mul x two) two) two n.
    Time Eval vm_compute in foo 100000000.

If we consider only the floating-point operations (by ignoring the cost of
the loop), the speedup is actually 30%.

0 files changed, 0 insertions, 0 deletions