compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Expand)	Author	Age	Files	Lines
*	Follow-up to commit 2613	xleroy	2014-08-20	1	-0/+2
*	PowerPC port: refactored the expansion of built-in functions and	xleroy	2014-07-28	1	-2/+45
*	Update for single-precision floats. Calls to vararg functions remain	xleroy	2014-07-24	1	-0/+16
*	Future-proofing: keep signature information in IA32 and PowerPC Asm, just lik...	xleroy	2013-12-26	1	-4/+4
*	powerpc/: new unary operation "addsymbol"	xleroy	2013-11-17	1	-0/+2
*	Update cchecklink w/ new Asm instructions Pmulh*	xleroy	2013-07-29	1	-0/+2
*	Updated to Pbuiltin with list of results	xleroy	2013-04-30	1	-1/+1
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20	1	-0/+1
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29	1	-14/+3
*	Revert unintentional commit #1955	xleroy	2012-07-06	1	-0/+0
*	Ajout trunk CompCert	blazy	2012-07-04	1	-0/+0
*	checklink: adaptation to the new floats	varobert	2012-07-03	1	-3/+3
*	Tracing each data chunk in debug mode	varobert	2012-04-04	1	-0/+9
*	checklink: first import of Valentin Robert's validator for asm and link	xleroy	2012-03-28	1	-0/+230