coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-10-06	Use OCaml floating-point operations on 64 bits arch	Pierre Roux
	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.