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

	Commit message (Expand)	Author	Age	Files	Lines
*	Bind some local defs with Let, makes extracted code cleanerv1.13	xleroy	2013-03-12	1	-2/+2
*	Maps: revised TREE interface; added mucho derived properties and operations i...	xleroy	2013-03-12	2	-63/+256
*	Suppress int64_unsigned_to_float, now unused.	xleroy	2013-03-11	2	-7/+0
*	More updates for 1.13	xleroy	2013-03-11	1	-2/+5
*	Fixed parsing of hex float literals 0xNNNpMMM.	xleroy	2013-03-11	5	-4/+81
*	Updated for version 1.13	xleroy	2013-03-11	2	-11/+24
*	Updating doc for 1.13	xleroy	2013-03-11	1	-8/+5
*	Useless Import	xleroy	2013-03-10	1	-1/+0
*	Glasnost: making transparent a number of definitions that were opaque	xleroy	2013-03-10	29	-120/+133
*	Assorted cleanups, esp. to avoid generating _rec and _rect recursors in	xleroy	2013-03-09	10	-215/+260
*	Improving the performance of exhaustive exploration (mode -all):	xleroy	2013-03-09	1	-18/+112
*	Finished backtracking (cf previous commit) for ARM and PowerPC.	xleroy	2013-03-04	7	-815/+593
*	Partial backtracking on previous commit: the "hole in Mach stack frame"	xleroy	2013-03-03	7	-857/+757
*	Updates to follow recent changes in PrintAsm.ml	xleroy	2013-03-01	1	-14/+43
*	Some builtins were renamed, updating	xleroy	2013-03-01	1	-4/+4
*	Bug in Pbtbl	xleroy	2013-03-01	1	-1/+1
*	No longer a dependency on Machtyping	xleroy	2013-03-01	2	-2/+1
*	Fix 'interp' entry	xleroy	2013-03-01	1	-1/+1
*	Testing dense switches	xleroy	2013-03-01	3	-1/+62
*	Revised Stacking and Asmgen passes and Mach semantics:	xleroy	2013-03-01	26	-7039/+4809
*	Updated ARM and PowerPC ports with new handling of __builtin_annot.	xleroy	2013-02-24	9	-90/+93
*	Constant propagation within __builtin_annot.	xleroy	2013-02-24	15	-124/+250
*	Pointers one past	xleroy	2013-02-15	21	-324/+565
*	Updated PowerPC port to new integers.	xleroy	2013-02-12	8	-29/+59
*	Be more like gcc in the way we display or not the usage message.	xleroy	2013-02-12	1	-8/+6
*	Forgot theorem "sign_ext_narrow".	xleroy	2013-02-12	1	-0/+12
*	lib/Integers.v: revised and extended, faster implementation based on	xleroy	2013-02-10	11	-1450/+1733
*	Some more properties. Refactored some proofs.	xleroy	2013-02-04	1	-21/+107
*	Typo in compare_mem causing merging of different states.	xleroy	2013-02-02	1	-1/+1
*	Errors for excessively large global variables or stack frames.	xleroy	2013-02-02	6	-14/+17
*	Camlcoq.ml: bug in conversion Z to stringv1.12.1	xleroy	2013-01-29	2	-4/+4
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29	69	-1024/+1173
*	Updated documentationv1.12	xleroy	2013-01-11	3	-15/+15
*	Update for release 1.12	xleroy	2013-01-09	4	-9/+27
*	Quote idents for safe re-parsing	xleroy	2013-01-08	1	-1/+1
*	Updated to new external functions and new representation of programs	xleroy	2013-01-08	1	-4/+15
*	More correct exportclight/ dependencies	xleroy	2013-01-08	2	-8/+9
*	Avoid generating some obviously useless casts.	xleroy	2013-01-08	2	-2/+36
*	Better treatment of volatile accesses in the reference interpreter.	xleroy	2013-01-08	2	-68/+83
*	Update Cminor parser and printer so that the parser can parse the whole Cmino...	xleroy	2013-01-07	5	-38/+107
*	Put clighgen files in exportclight/	xleroy	2013-01-05	6	-44/+99
*	Print Swhile loops. Fix indentation.	xleroy	2013-01-05	1	-8/+12
*	RTLgenaux: heuristic to orient if-then-else statements based on sizes.	xleroy	2012-12-31	2	-3/+62
*	Remove some useless "Require".	xleroy	2012-12-30	85	-235/+73
*	Make "all" the defaut target.	xleroy	2012-12-29	1	-18/+21
*	Merge of the clightgen branch:	xleroy	2012-12-29	34	-2718/+4800
*	Fix "clean" rule.	xleroy	2012-12-29	1	-1/+1
*	Composition properties between injections and extensions.	xleroy	2012-12-29	1	-8/+80
*	Integers: specialized function to compute x mod 2^N; used in "repr" to	xleroy	2012-12-21	2	-115/+179
*	Separate interference graphs for ints and floats, i.e. don't record interfere...	xleroy	2012-12-20	1	-13/+16