compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Remove coq warnings (#28)	Bernhard Schommer	2017-09-22	1	-1/+1
\| \| \| \|	Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
*	Updated PR by removing whitespaces. Bug 17450.	Bernhard Schommer	2015-10-20	1	-37/+37
\|
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29	1	-5/+5
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Process successors in increasing order. Helps preserving the nice CFG	xleroy	2012-07-01	1	-23/+62
\| \| \| \| \| \| \| \|	structure that we got from Cminorgen. Otherwise, the linearization heuristic can produce rather bad code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1948 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of the newmem branch:	xleroy	2012-05-21	1	-0/+316
	- Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e