compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Expand)	Author	Age	Files	Lines
*	Removing modules now unused	xleroy	2013-05-01	1	-867/+0
*	Assorted changes to reduce stack and heap requirements when compiling very bi...	xleroy	2013-03-16	1	-3/+6
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29	1	-4/+2
*	Separate interference graphs for ints and floats, i.e. don't record interfere...	xleroy	2012-12-20	1	-13/+16
*	powerpc/SelectOp: optimize the pattern ((x >>s N) & N1) & N2 common in a cert...	xleroy	2012-01-21	1	-11/+28
*	Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml chars	xleroy	2011-10-18	1	-4/+4
*	Coloringaux: better cost estimate for annotation builtins	xleroy	2011-06-14	1	-0/+2
*	Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.	xleroy	2011-03-09	1	-3/+2
*	Merge of the reuse-temps branch:	xleroy	2010-09-02	1	-37/+56
*	Merge of branches/full-expr-4:	xleroy	2010-08-18	1	-9/+18
*	Support for inlined built-ins.	xleroy	2010-06-29	1	-4/+6
*	Improved coalescing heuristics based on Hailperin's paper.	xleroy	2010-05-08	1	-32/+49
*	Compute spill costs.	xleroy	2010-05-02	1	-8/+92
*	Coloring: allow to exclude user-specified registers from allocation.	xleroy	2010-04-10	1	-25/+40
*	Coloringaux: make identifiers unique; special treatment of precolored	xleroy	2009-08-26	1	-60/+132
*	Update spill costs when coalescing	xleroy	2009-08-16	1	-2/+3
*	Reorganized the development, modularizing away machine-dependent parts.	xleroy	2008-12-30	1	-0/+626