coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-11-18	Add more explicit tests for next_up and next_down.	Pierre Roux

2020-08-09	Bring Float notations in line with stdlib	Jason Gross
	This is a companion to #12479 as per https://github.com/coq/coq/pull/12479#issuecomment-641336039 that changes some of the PrimFloat notations: - `m == n` into `m =? n` to correspond with the eqb notations elsewhere - `m < n` into `m <? n` to correspond with the ltb notations elsewhere - `m <= n` into `m <=? n` to correspond with the leb notations elsewhere We also put them in a module, so users can `Require PrimFloat. Import PrimFloat.PrimFloatNotations` without needing to unqualify the primitives. Fixes the part of #12454 about floats
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	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	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	Parsing primitive float constants	Pierre Roux

2019-11-01	Add tests for primitive floats with 'native_compute'	Pierre Roux
	Tests are updated to include native computations.
2019-11-01	Add next_{up,down} primitive float functions	Pierre Roux

2019-11-01	Implement classify on primitive float	Pierre Roux

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.