compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Upgrade Flocq to version 2.6.1 from upstream (#71)	Xavier Leroy	2018-04-25	1	-30/+32
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We were previously at 2.5.2. Quoting the NEWS from upstream: Version 2.6.1: - ensured compatibility from Coq 8.4 to 8.8 Version 2.6.0: - ensured compatibility from Coq 8.4 to 8.7 - removed some hypotheses on some lemmas of Fcore_ulp - added lemmas to Fprop_plus_error - improved examples Also: in preparation for Coq 8.8, silence warning "compatibility-notation" when building Flocq, because this warning is on by default in 8.8, and Flocq triggers it a lot.
*	Adapt proofs to future handling of literal constants in Coq.	Guillaume Melquiond	2017-03-08	1	-14/+16
\| \| \| \| \| \|	This commit is mainly a squash of the relevant compatibility commits from Flocq's master. Most of the changes are meant to make the proofs oblivious to the way constants such as 0, 1, 2, and -1 are represented.
*	Upgrade to Flocq 2.5.0.	Guillaume Melquiond	2015-09-22	1	-73/+106
\| \| \| \|	Note: this version of Flocq is compatible with both Coq 8.4 and 8.5.
*	Upgrade to flocq 2.4.0	Jacques-Henri Jourdan	2014-10-07	1	-0/+4554