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	-1/+1
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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.
*	Update Flocq to version 2.5.2	Xavier Leroy	2017-02-13	1	-1/+1
\| \| \| \|	This version of Flocq is compatible with Coq 8.6
*	Upgrade to Flocq 2.5.0.	Guillaume Melquiond	2015-09-22	1	-2/+3
\| \| \| \|	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	-1/+1
\|
*	Merge of Flocq version 2.2.0.	xleroy	2013-08-02	1	-3/+3
\| \| \| \| \| \| \|	More precise modeling of NaNs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2303 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Use Flocq for floats	xleroy	2012-06-28	1	-0/+31
	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e