coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2020-02-26	Consolidate int63-related notations	Maxime Dénès
	We avoid redundant notations for the same concepts and make sure notations do not break Ltac parsing for users of these libraries.
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	docs: Add refman+stdlib documentation	Erik Martin-Dorel

2019-11-01	Add next_{up,down} primitive float functions	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.