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

	Commit message (Expand)	Author	Age	Files	Lines
...
*	Glasnost: making transparent a number of definitions that were opaque	xleroy	2013-03-10	1	-2/+2
*	Assorted cleanups, esp. to avoid generating _rec and _rect recursors in	xleroy	2013-03-09	1	-0/+4
*	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	1	-1285/+1593
*	Some more properties. Refactored some proofs.	xleroy	2013-02-04	1	-21/+107
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29	1	-5/+5
*	Integers: specialized function to compute x mod 2^N; used in "repr" to	xleroy	2012-12-21	1	-114/+177
*	Micro-optimization of (x & mask) >>s amount into a rolm when mask >= 0.	xleroy	2012-07-09	1	-0/+46
*	Changelog: updated	xleroy	2012-06-28	1	-0/+40
*	More properties on mul/div/mod	xleroy	2012-06-09	1	-0/+39
*	More aggressive common subexpression elimination (CSE) of memory loads.	xleroy	2012-02-23	1	-0/+50
*	Merge of the nonstrict-ops branch:	xleroy	2012-01-14	1	-20/+127
*	Changelog, doc: updated for release 1.9v1.9	xleroy	2011-08-22	1	-8/+7
*	Back from Oregon commit.	xleroy	2011-07-05	1	-0/+10
*	Relating neg and not	xleroy	2011-06-22	1	-5/+42
*	Merge of branch "unsigned-offsets":	xleroy	2011-04-09	1	-23/+139
*	Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_ext	xleroy	2010-08-21	1	-1024/+1009
*	Merging the Princeton implementation of the memory model. Separate axioms in...	xleroy	2010-06-28	1	-1/+2
*	Revised encoding/decoding of floats	xleroy	2010-05-09	1	-1/+13
*	More theorems about sign and zero extensions	xleroy	2010-05-05	1	-0/+100
*	Merge of the newmem and newextcalls branches:	xleroy	2010-03-07	1	-4/+11
*	Revised lib/Integers.v to make it parametric w.r.t. word size.	xleroy	2009-11-19	1	-389/+481
*	More realistic treatment of jump tables: show the absence of overflow when ac...	xleroy	2009-11-10	1	-0/+7
*	Added support for jump tables in back end.	xleroy	2009-11-10	1	-0/+25
*	Adapted to work with Coq 8.2-1v1.4.1	xleroy	2009-06-05	1	-3/+3
*	Reserve register GPR13 for compatibility with EABI. Optimize operations 'x >...	xleroy	2009-02-26	1	-0/+20
*	- Added alignment constraints to memory loads and stores.	xleroy	2009-01-11	1	-53/+0
*	Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.	xleroy	2008-12-29	1	-258/+638
*	Ajout license, README, copyright notices	xleroy	2008-01-27	1	-0/+15
*	Preuve des 2 axiomes restants	xleroy	2007-03-02	1	-2/+17
*	Petites adaptations pour Coq 8.1gamma	xleroy	2006-11-11	1	-14/+22
*	Fusion de la branche "traces":	xleroy	2006-09-04	1	-36/+35
*	Initial import of compcert	xleroy	2006-02-09	1	-0/+2184