compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Expand)	Author	Age	Files	Lines
*	Represent struct and union types by name instead of by structure.	Xavier Leroy	2014-12-22	1	-93/+109
*	Add Genv.public_symbol operation.	Xavier Leroy	2014-11-24	1	-3/+9
*	- Support "switch" statements over 64-bit integers	xleroy	2014-08-17	1	-3/+7
*	Merge of "newspilling" branch:	xleroy	2014-07-23	1	-32/+25
*	Remove useless checks on type_of_global in dynamic semantics	xleroy	2014-02-20	1	-12/+1
*	Ctypes.sizeof ty = 0 for empty types ty (zero-sized array, empty struct/union).	xleroy	2013-12-30	1	-38/+85
*	Simpler, more robust emulation of calls to variadic functions:	xleroy	2013-12-28	1	-2/+2
*	Support "default" cases in the middle of a "switch", not just at the end.	xleroy	2013-12-21	1	-12/+58
*	Revised treatment of _Alignas, for better compatibility with GCC and Clang, a...	xleroy	2013-11-06	1	-7/+11
*	Merge of the "alignas" branch.	xleroy	2013-10-05	1	-8/+10
*	Revised handling of int->float conversions:	xleroy	2013-07-08	1	-1/+4
*	Treat casts int64 -> float32 as primitive operations instead of two	xleroy	2013-07-03	1	-1/+2
*	Merge of the "princeton" branch:	xleroy	2013-06-16	1	-83/+82
*	driver: removed option -flonglong	xleroy	2013-04-22	1	-0/+4
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20	1	-196/+48
*	Pointers one past	xleroy	2013-02-15	1	-18/+27
*	lib/Integers.v: revised and extended, faster implementation based on	xleroy	2013-02-10	1	-3/+3
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29	1	-26/+26
*	Avoid generating some obviously useless casts.	xleroy	2013-01-08	1	-1/+22
*	Merge of the clightgen branch:	xleroy	2012-12-29	1	-0/+2277