coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-06-08	Fix 12483	Pierre Roux

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	docs: Add refman+stdlib documentation	Erik Martin-Dorel

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	Add next_{up,down} primitive float functions	Pierre Roux

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

2019-11-01	Put axioms on ldshiftexp and frshiftexp	Guillaume Bertholon
	Axioms on ldexp and frexp are replaced by proofs inside FloatLemmas. The shift value has been increased to 2 * emax + prec because in ldexp we want to be able to transform the smallest denormalized to the biggest float value in one call.
2019-11-01	Add Floats to standard library	Guillaume Bertholon
	All supported floating point operations are defined on specification floats. Then we register the primitive type and functions, and add conversion functions to and from the specification type. Finally we put axioms to state that primitive operations behave exactly the same as specification operations. CREDITS: Most of the code inside SpecFloat is adapted from the Flocq library. NOTE: For the moment this code will not compile if native compilation is enabled in the configuration phase. This will be resolved later when native_compute will be supported by primitive floats. So please use option "-native-compiler no" in ./configure currently.