coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-11-01	Fix ldshiftexp	Pierre Roux
	* Fix the implementations and add tests * Change shift from int63 to Z (was always used as a Z) * Update FloatLemmas.v accordingly Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
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.
2019-11-01	Add tests for primitive floats with 'native_compute'	Pierre Roux
	Tests are updated to include native computations.
2019-11-01	Add tests for primitive floats with 'vm_compute'	Guillaume Bertholon
	Tests are updated to include VM computations and check for double rounding.
2019-11-01	Add tests for primitive floats	Guillaume Bertholon
	Add utility ldexp and frexp functions to prevent dealing with the shift of ldshiftexp and frshiftexp everywhere. Also move primitive integer tests to place all primitive tests in the same directory.