compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Incompatibility 8.3 / 8.3pl1	xleroy	2011-03-14	1	-1/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1606 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Slightly nicer semantics for initialization	xleroy	2011-03-13	1	-28/+29
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1604 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	More global initialization work done and proved in Coq.	xleroy	2011-03-13	1	-12/+312
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1603 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Initializers for global variables: compile-time evaluation of expressions ↵	xleroy	2011-03-12	1	-0/+555
	done in Coq (module Initializers), using the same primitives as those for CompCert C's semantics. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1602 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e