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

	Commit message (Expand)	Author	Age	Files	Lines
*	[BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...	Cyril SIX	2021-06-01	1	-4/+5
*	Support for 64-bit architectures: generic support	Xavier Leroy	2016-10-01	1	-4/+4
*	common/Determinism.v: dual-license with GPL	Xavier Leroy	2016-06-30	1	-0/+3
*	Updated PR by removing whitespaces. Bug 17450.	Bernhard Schommer	2015-10-20	1	-46/+46
*	Use Coq strings instead of idents to name external and builtin functions.	Xavier Leroy	2015-10-11	1	-2/+3
*	Represent external worlds by a coinductive type rather than an inductive type.	Xavier Leroy	2015-06-07	1	-1/+1
*	Make small-step semantics more parametric w.r.t. the type of global environme...	Xavier Leroy	2014-11-26	1	-5/+5
*	Remove some useless "Require".	xleroy	2012-12-30	1	-1/+0
*	Removed old, commented-out definitions.	xleroy	2012-08-01	1	-292/+30
*	Cleaned up old commented-out parts	xleroy	2011-08-19	1	-19/+0
*	Added animation of the CompCert C semantics (ccomp -interp)	xleroy	2011-07-28	1	-54/+55
*	Merge of branch new-semantics: revised and strengthened top-level statements ...	xleroy	2011-07-15	1	-102/+155
*	Merge of branches/full-expr-4:	xleroy	2010-08-18	1	-137/+373
*	- Extended traces so that pointers within globals are supported as event values.	xleroy	2010-05-10	1	-11/+23
*	Merge of the newmem and newextcalls branches:	xleroy	2010-03-07	1	-62/+80
*	Distinguish two kinds of nonterminating behaviors: silent divergence	xleroy	2009-08-16	1	-0/+508