debian-compcert - Debian packaging for CompCert

	Commit message (Expand)	Author	Age
*	Use "-as" to put CompCert modules in a compcert.xxx namespace.	xleroy	2013-05-01
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20
*	Updated issues with coqchk. See PR#3026 on the Coq bug tracker.	xleroy	2013-04-14
*	Assorted changes to reduce stack and heap requirements when compiling very bi...	xleroy	2013-03-16
*	Revised Stacking and Asmgen passes and Mach semantics:	xleroy	2013-03-01
*	More correct exportclight/ dependencies	xleroy	2013-01-08
*	Put clighgen files in exportclight/	xleroy	2013-01-05
*	RTLgenaux: heuristic to orient if-then-else statements based on sizes.	xleroy	2012-12-31
*	Make "all" the defaut target.	xleroy	2012-12-29
*	Merge of the clightgen branch:	xleroy	2012-12-29
*	Clight: split off the big step semantics in ClightBigstep.	xleroy	2012-10-14
*	Make Clight independent of CompCert C.	xleroy	2012-10-08
*	Support for indirect symbols under MacOS X (final).	xleroy	2012-07-14
*	Revert unintentional commit #1955	xleroy	2012-07-06
*	Ajout trunk CompCert	blazy	2012-07-04
*	Use Flocq for floats	xleroy	2012-06-28
*	CSE: add recognition of some combined operators, conditions, and addressing m...	xleroy	2012-05-26
*	Merge of the newmem branch:	xleroy	2012-05-21
*	Configuration, build and install for cchecklink. Clean-ups in myocamlbuild.ml.	xleroy	2012-04-04
*	checklink: first import of Valentin Robert's validator for asm and link	xleroy	2012-03-28
*	make clean must erase tools/ndfun	xleroy	2012-03-13
*	Cosmetic cleanups.	xleroy	2012-01-15
*	Merge of the nonstrict-ops branch:	xleroy	2012-01-14
*	Changelog, doc: updated for release 1.9	xleroy	2011-08-22
*	New backend pass "RRE": optimize (somewhat) redundant reloads introduced by t...	xleroy	2011-08-16
*	ARM codegen ported to new ABI + VFD floats	xleroy	2011-07-30
*	Updated Makefile and dependencies. Typo in powerpc/PrintAsm.ml.	xleroy	2011-07-28
*	Added animation of the CompCert C semantics (ccomp -interp)	xleroy	2011-07-28
*	Merge of branch new-semantics: revised and strengthened top-level statements ...	xleroy	2011-07-15
*	Added pass CleanupLabels to remove unreferenced labels in a proved way.	xleroy	2011-05-08
*	Renamed Machconcr into Machsem.	xleroy	2011-04-09
*	Merge of branch "unsigned-offsets":	xleroy	2011-04-09
*	Initializers for global variables: compile-time evaluation of expressions don...	xleroy	2011-03-12
*	Revised signed/unsigned char handling.	xleroy	2011-03-10
*	Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.	xleroy	2011-03-09
*	Treat "char" as unsigned OR signed depending on the configuration.	xleroy	2011-03-09
*	Various algorithmic improvements that reduce compile times (thanks Alexandre ...	xleroy	2010-10-27
*	Updates for IA32-Cygwin.	xleroy	2010-09-08
*	Simplified stdlib wrapper; use it only under MacOS X	xleroy	2010-09-04
*	Removed useless constraints on return type at Sreturn instructions	xleroy	2010-08-18
*	Merge of branches/full-expr-4:	xleroy	2010-08-18
*	Support for inlined built-ins.	xleroy	2010-06-29
*	Merging the Princeton implementation of the memory model. Separate axioms in...	xleroy	2010-06-28
*	Cleaner generation of .depend	xleroy	2010-03-30
*	New HTML documentation generator	xleroy	2010-03-09
*	Merge of the newmem and newextcalls branches:	xleroy	2010-03-07
*	Suppressed Init_pointer, now useless. Improved printing of strings in genera...	xleroy	2010-03-03
*	Switching to the new C parser/elaborator/simplifier	xleroy	2010-03-03
*	Coloringaux: make identifiers unique; special treatment of precolored	xleroy	2009-08-26
*	Build bytecode version with debug symbols.	xleroy	2009-08-20