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

	Commit message (Collapse)	Author	Age	Files	Lines
*	[BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵	Cyril SIX	2021-06-01	1	-4/+5
\| \| \| \|	cfrontend/C2C.ml
*	Replace `omega` tactic with `lia`	Xavier Leroy	2020-12-29	1	-2/+2
\| \| \| \| \| \| \| \| \| \| \|	Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
*	Remove coq warnings (#28)	Bernhard Schommer	2017-09-22	1	-1/+1
\| \| \| \|	Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
*	Updated PR by removing whitespaces. Bug 17450.	Bernhard Schommer	2015-10-20	1	-37/+37
\|
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29	1	-5/+5
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Process successors in increasing order. Helps preserving the nice CFG	xleroy	2012-07-01	1	-23/+62
\| \| \| \| \| \| \| \|	structure that we got from Cminorgen. Otherwise, the linearization heuristic can produce rather bad code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1948 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of the newmem branch:	xleroy	2012-05-21	1	-0/+316
	- Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e