debian-compcert - Debian packaging for CompCert

	Commit message (Expand)	Author	Age
*	Merge of "newspilling" branch:	xleroy	2014-07-23
*	Refactoring: move symbol_offset into Genv.	xleroy	2014-05-24
*	Updated the proofs.	xleroy	2014-04-12
*	Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ove...	xleroy	2014-04-09
*	Add option -Os to optimize for code size rather than for execution speed.	xleroy	2014-02-19
*	powerpc/: new unary operation "addsymbol"	xleroy	2013-11-17
*	Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms	xleroy	2013-09-14
*	Optimize integer divisions by positive constants, turning them into	xleroy	2013-07-29
*	Updated to new CminorSel	xleroy	2013-04-30
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29
*	Remove some useless "Require".	xleroy	2012-12-30
*	Merge of branch seq-and-or. See Changelog for details.	xleroy	2012-10-06
*	Remove Val.is_true and Val.is_false, no longer used.	xleroy	2012-08-06
*	Micro-optimization of (x & mask) >>s amount into a rolm when mask >= 0.	xleroy	2012-07-09
*	Factor out the evaluation of the float constant in intuoffloat.	xleroy	2012-07-01
*	CSE: add recognition of some combined operators, conditions, and addressing m...	xleroy	2012-05-26
*	Hack with nxor	xleroy	2012-05-18
*	PowerPC: remove the fmadd and fmsub operators/Asm instructions	xleroy	2012-03-07
*	Take advantage of Cmaskzero and Cmasknotzero.	xleroy	2012-02-24
*	Improved instruction selection for "notint".	xleroy	2012-02-24
*	Merge of the "volatile" branch:	xleroy	2012-02-04
*	powerpc/SelectOp: optimize the pattern ((x >>s N) & N1) & N2 common in a cert...	xleroy	2012-01-21
*	Merge of the nonstrict-ops branch:	xleroy	2012-01-14
*	Recognition of rlwimi instruction (useful for bitfield assignment)	xleroy	2011-06-21
*	Merge of branch "unsigned-offsets":	xleroy	2011-04-09
*	float->int conversions, continued: weaker axiomatization.	xleroy	2010-10-29
*	Float.intoffloat and Float.intuoffloat are now partial functions.	xleroy	2010-10-28
*	Merge of the reuse-temps branch:	xleroy	2010-09-02
*	Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_ext	xleroy	2010-08-21
*	Optimisation: addrsymbol + (expr + cst) and addrstack + (expr + cst).	xleroy	2010-05-02
*	Merge of the newmem and newextcalls branches:	xleroy	2010-03-07
*	Wrong rlwinm generated for 'x mod 1'	xleroy	2010-03-02
*	Revised lib/Integers.v to make it parametric w.r.t. word size.	xleroy	2009-11-19
*	Refactored Selection.v and Selectionproof.v into a machine-dependent part + a...	xleroy	2009-08-17