compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Expand)	Author	Age	Files	Lines
*	Memory.v: added drop_perm operation	xleroy	2010-09-21	1	-24/+62
*	Merging the Princeton implementation of the memory model. Separate axioms in...	xleroy	2010-06-28	1	-0/+1
*	More faithful semantics for volatile reads and writes.	xleroy	2010-05-23	1	-83/+110
*	- Extended traces so that pointers within globals are supported as event values.	xleroy	2010-05-10	1	-36/+34
*	Merge of the newmem and newextcalls branches:	xleroy	2010-03-07	1	-791/+942
*	Adapted to work with Coq 8.2-1v1.4.1	xleroy	2009-06-05	1	-53/+53
*	Ajout license, README, copyright notices	xleroy	2008-01-27	1	-0/+15
*	Ajout find_symbol_not_nullptr; nettoyages	xleroy	2007-12-06	1	-39/+71
*	Ajout de global_addresses_distinct	xleroy	2007-11-03	1	-16/+75
*	Fusion des modifications faites sur les branches "tailcalls" et "smallstep".	xleroy	2007-08-04	1	-173/+517
*	Revu traitement des variables globales dans AST.program et dans Globalenvs.	xleroy	2006-09-05	1	-158/+222
*	Revu la repartition des sources Coq en sous-repertoires	xleroy	2006-09-04	1	-0/+643