coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-11-13	Turn coq_float64.h into a .c file as it is no longer needed by coq_interp.c.	Guillaume Melquiond

2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-11-01	Add "==", "<", "<=" in PrimFloat.v	Erik Martin-Dorel
	* Add a related test-suite in compare.v (generated by a bash script) Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
2019-11-01	Reimplement is_float	Pierre Roux
	is_float was relying on Obj.tag triggering a check that we are in the OCaml heap which is expensive. On extreme examples, this can lead to a global 2x speedup. Thanks to Maxime Dénès and Jacques-Henri Jourdan for their help in diagnosing this.
2019-11-01	Make primitive float work on x86_32	Pierre Roux
	Flag -fexcess-precision=standard is not enough on x86_32 where -msse2 -mfpmath=sse is required (-msse is not enough) to avoid double rounding issues in the VM. Most floating-point operation are now implemented in C because OCaml is suffering double rounding issues on x86_32 with 80 bits extended precision registers used for floating-point values, causing double rounding making floating-point arithmetic incorrect with respect to its specification. Add a runtime test for double roundings.