debian-compcert - Debian packaging for CompCert

	Commit message (Expand)	Author	Age
*	Revised Stacking and Asmgen passes and Mach semantics:	xleroy	2013-03-01
*	Updated ARM and PowerPC ports with new handling of __builtin_annot.	xleroy	2013-02-24
*	Constant propagation within __builtin_annot.	xleroy	2013-02-24
*	Pointers one past	xleroy	2013-02-15
*	Updated PowerPC port to new integers.	xleroy	2013-02-12
*	Be more like gcc in the way we display or not the usage message.	xleroy	2013-02-12
*	Forgot theorem "sign_ext_narrow".	xleroy	2013-02-12
*	lib/Integers.v: revised and extended, faster implementation based on	xleroy	2013-02-10
*	Some more properties. Refactored some proofs.	xleroy	2013-02-04
*	Typo in compare_mem causing merging of different states.	xleroy	2013-02-02
*	Errors for excessively large global variables or stack frames.	xleroy	2013-02-02
*	Camlcoq.ml: bug in conversion Z to string	xleroy	2013-01-29
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29
*	Updated documentation	xleroy	2013-01-11
*	Update for release 1.12	xleroy	2013-01-09
*	Quote idents for safe re-parsing	xleroy	2013-01-08
*	Updated to new external functions and new representation of programs	xleroy	2013-01-08
*	More correct exportclight/ dependencies	xleroy	2013-01-08
*	Avoid generating some obviously useless casts.	xleroy	2013-01-08
*	Better treatment of volatile accesses in the reference interpreter.	xleroy	2013-01-08
*	Update Cminor parser and printer so that the parser can parse the whole Cmino...	xleroy	2013-01-07
*	Put clighgen files in exportclight/	xleroy	2013-01-05
*	Print Swhile loops. Fix indentation.	xleroy	2013-01-05
*	RTLgenaux: heuristic to orient if-then-else statements based on sizes.	xleroy	2012-12-31
*	Remove some useless "Require".	xleroy	2012-12-30
*	Make "all" the defaut target.	xleroy	2012-12-29
*	Merge of the clightgen branch:	xleroy	2012-12-29
*	Fix "clean" rule.	xleroy	2012-12-29
*	Composition properties between injections and extensions.	xleroy	2012-12-29
*	Integers: specialized function to compute x mod 2^N; used in "repr" to	xleroy	2012-12-21
*	Separate interference graphs for ints and floats, i.e. don't record interfere...	xleroy	2012-12-20
*	Test bitfields of enum type	xleroy	2012-12-18
*	Support for inline assembly (asm statements).	xleroy	2012-12-18
*	Test for __builtin_fcti	xleroy	2012-11-24
*	Add __builtin_fcti (double -> int conversion w/ round to nearest)	xleroy	2012-11-24
*	Globalenvs: allocate one-byte block with permissions Nonempty for each	xleroy	2012-11-12
*	Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)	xleroy	2012-11-03
*	Update cparser/Makefile (fix by Jacques-Henri Jourdan)	xleroy	2012-11-03
*	Clight: split off the big step semantics in ClightBigstep.	xleroy	2012-10-14
*	Generate output files in current directory; can be overriden with -o option	xleroy	2012-10-08
*	Make Clight independent of CompCert C.	xleroy	2012-10-08
*	Merge of branch seq-and-or. See Changelog for details.	xleroy	2012-10-06
*	Fixed 2 errors in revised builtin_vstore.	xleroy	2012-08-22
*	Wrong usage of temps in builtin_volatile_write.	xleroy	2012-08-17
*	Define useful functions instr_defs and instr_uses	xleroy	2012-08-10
*	Remove Val.is_true and Val.is_false, no longer used.	xleroy	2012-08-06
*	Updated documentation	xleroy	2012-08-02
*	Removed old, commented-out definitions.	xleroy	2012-08-01
*	More aggressive elimination of conditional branches during constant	xleroy	2012-08-01
*	Forgot to collect types of expressions	xleroy	2012-07-28