coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-11-01	Add tests for primitive floats with 'native_compute'	Pierre Roux
	Tests are updated to include native computations.
2019-11-01	Change return type of primitive float comparison	Pierre Roux
	Replace `option comparison` with `float_comparison` (:= `FEq \| FLt \| FGt \| FNotComparable`) as suggested by Guillaume Melquiond to avoid boxing and an extra match when using primitive float comparison.
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.