compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Expand)	Author	Age	Files	Lines
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20	1	-1/+4
*	Updated ARM and PowerPC ports with new handling of __builtin_annot.	xleroy	2013-02-24	1	-13/+0
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29	1	-8/+8
*	Make min_int / -1 and min_int % -1 semantically undefined	xleroy	2012-06-09	1	-1/+2
*	Merge of the newmem branch:	xleroy	2012-05-21	1	-2/+24
*	Support for fcmpzd instruction (float compare with +0.0)	xleroy	2012-03-29	1	-0/+9
*	Added volatile_read_global and volatile_store_global builtins.	xleroy	2012-01-15	1	-0/+14
*	Merge of the nonstrict-ops branch:	xleroy	2012-01-14	1	-358/+245
*	ARM codegen ported to new ABI + VFD floats	xleroy	2011-07-30	1	-0/+2
*	Merge of branch "unsigned-offsets":	xleroy	2011-04-09	1	-55/+56
*	Float.intoffloat and Float.intuoffloat are now partial functions.	xleroy	2010-10-28	1	-0/+2
*	Merge of the newmem and newextcalls branches:	xleroy	2010-03-07	1	-1/+1
*	Revised lib/Integers.v to make it parametric w.r.t. word size.	xleroy	2009-11-19	1	-8/+8
*	"val_match_approx_increasing" moved from mach-dep part to mach-indep part.	xleroy	2009-08-18	1	-11/+0
*	Refactoring of Constprop and Constpropproof into a machine-dependent part and...	xleroy	2009-08-17	1	-0/+541