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

	Commit message (Expand)	Author	Age	Files	Lines
*	Define `fold_ind_aux` and `fold_ind` transparently	Xavier Leroy	2021-01-21	1	-2/+2
*	Add new fold_ind induction principle for folds	Xavier Leroy	2021-01-13	1	-63/+82
*	Replace `omega` tactic with `lia`	Xavier Leroy	2020-12-29	1	-1/+1
*	Coq 8.10 compatibility: tweak Argument command	Xavier Leroy	2019-08-05	1	-1/+1
*	Hybrid 64bit/32bit PowerPC port	Bernhard Schommer	2017-05-03	1	-9/+9
*	Replace "Implicit Arguments" with "Arguments"	Xavier Leroy	2017-02-13	1	-2/+2
*	Port to Coq 8.5pl2	Xavier Leroy	2016-07-08	1	-51/+51
*	ValueAnalysis: use ZTrees instead of ZMaps for abstracting contents of memory...	Xavier Leroy	2016-05-07	1	-0/+80
*	Preliminaries: extend the Coqlib and Maps libraries.	Xavier Leroy	2016-03-06	1	-34/+133
*	Updated PR by removing whitespaces. Bug 17450.	Bernhard Schommer	2015-10-20	1	-113/+113
*	remove not used hypotheses in TREE	Jacques-Henri Jourdan	2015-03-25	1	-9/+4
*	Add theorem "elements_remove".	Xavier Leroy	2014-09-24	1	-167/+178
*	More efficient implementations of map, fold, etc.	xleroy	2014-08-27	1	-164/+109
*	Small improvements in compilation times for the register allocation pass.	xleroy	2013-09-20	1	-0/+39
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20	1	-330/+194
*	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	1	-59/+248
*	Useless Import	xleroy	2013-03-10	1	-1/+0
*	Glasnost: making transparent a number of definitions that were opaque	xleroy	2013-03-10	1	-34/+52
*	Assorted cleanups, esp. to avoid generating _rec and _rect recursors in	xleroy	2013-03-09	1	-21/+5
*	Memdata: cleanup continued	xleroy	2012-05-26	1	-0/+26
*	Merge of the newmem branch:	xleroy	2012-05-21	1	-4/+96
*	Cleaned up old commented-out parts	xleroy	2011-08-19	1	-5/+0
*	Various algorithmic improvements that reduce compile times (thanks Alexandre ...	xleroy	2010-10-27	1	-2/+22
*	Merge of the newmem and newextcalls branches:	xleroy	2010-03-07	1	-0/+77
*	Coloringaux: make identifiers unique; special treatment of precolored	xleroy	2009-08-26	1	-42/+56
*	Cil2Csyntax: added goto and labels; added assignment between structs	xleroy	2009-08-16	1	-1/+35
*	Added 'going wrong' behaviors	xleroy	2009-08-05	1	-0/+115
*	Adapted to work with Coq 8.2-1v1.4.1	xleroy	2009-06-05	1	-130/+130
*	Suppression de 'exten', inutilise	xleroy	2008-05-30	1	-6/+0
*	Ajout license, README, copyright notices	xleroy	2008-01-27	1	-0/+15
*	Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de...	xleroy	2007-03-02	1	-0/+82
*	Ajout operation eq dans PMap et IndexedMap	xleroy	2007-01-03	1	-0/+10
*	Initial import of compcert	xleroy	2006-02-09	1	-0/+1034