compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Change Implicit Arguments to Arguments (#225)	Jasper Hugunin	2018-03-28	1	-7/+7
\| \| \| \| \| \| \|	Implicit Arguments is deprecated in Coq since 8.6 or so. Some Implicit Arguments remained in Flocq but were recently changed to Arguments. Apply the same change to our local copy of Flocq. As a positive consequence, we no longer need to suppress the deprecation warnings while compiling Flocq.
*	Upgrade to Flocq 2.5.0.	Guillaume Melquiond	2015-09-22	1	-2/+2
\| \| \| \|	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	-71/+144
\|
*	Merge of "newspilling" branch:	xleroy	2014-07-23	1	-0/+51
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of Flocq version 2.2.0.	xleroy	2013-08-02	1	-25/+43
\| \| \| \| \| \| \|	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/+546
	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e