compcert-kvx - Unnamed repository; edit this file 'description' to name the repository.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Ensure FunInd or Recdef is imported if functional induction is used	Sigurd Schneider	2017-07-20	1	-0/+1
\| \| \| \| \| \|	Coq 8.7 does not load FunInd in prelude anymore, so this is necessary. Recdef exports FunInd, so if Recdef is imported, importing FunInd is not required.
*	Updated PR by removing whitespaces. Bug 17450.	Bernhard Schommer	2015-10-20	1	-23/+23
\|
*	Merge of branch value-analysis.	xleroy	2013-12-20	1	-38/+42
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fine-tuning of the "andimm" case to generate a move rather than an andimm ↵	xleroy	2013-10-24	1	-0/+7
\| \| \| \| \| \|	when possible. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2348 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Deactivate combination Aindexed 0 / Oadd, as it causes problems with chunk = ↵	xleroy	2013-04-21	1	-3/+0
\| \| \| \| \| \|	Mint64. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2210 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Recombine x = cmp(...); if (x == 1) ...	xleroy	2012-07-01	1	-0/+33
\| \| \| \| \| \| \|	and x = cmp(...); if (x != 1) ... git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1946 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	CSE: add recognition of some combined operators, conditions, and addressing ↵	xleroy	2012-05-26	1	-0/+142
	modes (cf. CombineOp.v) Memory model: cleaning up Memdata Inlining and new Constprop: updated for ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1902 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e