compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Reorganized the development, modularizing away machine-dependent parts.	xleroy	2008-12-30	1	-85/+0
\| \| \| \| \| \| \| \| \|	Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Extract Coq lists to Caml lists.	xleroy	2008-12-29	1	-2/+2
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@929 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout license, README, copyright notices	xleroy	2008-01-27	1	-0/+12
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revu l'heuristique de linearisation	xleroy	2007-10-30	1	-46/+36
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@438 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFG	xleroy	2007-10-27	1	-0/+83
	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@437 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e