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

	Commit message (Expand)	Author	Age	Files	Lines
...
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29	1	-3/+9
*	Remove some useless "Require".	xleroy	2012-12-30	1	-2/+0
*	Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)	xleroy	2012-11-03	1	-3/+39
*	Changelog: updated	xleroy	2012-06-28	1	-0/+14
*	Use Flocq for floats	xleroy	2012-06-28	1	-52/+725
*	float->int conversions, continued: weaker axiomatization.	xleroy	2010-10-29	1	-22/+3
*	Float.intoffloat and Float.intuoffloat are now partial functions.	xleroy	2010-10-28	1	-6/+25
*	Merge of the reuse-temps branch:	xleroy	2010-09-02	1	-17/+101
*	Fewer float axioms.	xleroy	2010-05-09	1	-4/+2
*	Suppressed axioms Float.eq_zero_{true,false}, since the latter is	xleroy	2010-05-09	1	-3/+0
*	Revised encoding/decoding of floats	xleroy	2010-05-09	1	-0/+18
*	Adapted to work with Coq 8.2-1v1.4.1	xleroy	2009-06-05	1	-1/+1
*	Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...	xleroy	2008-05-30	1	-0/+1
*	Ajout license, README, copyright notices	xleroy	2008-01-27	1	-0/+15
*	Petites adaptations pour Coq 8.1gamma	xleroy	2006-11-11	1	-1/+1
*	Fusion de la branche "traces":	xleroy	2006-09-04	1	-1/+0
*	Initial import of compcert	xleroy	2006-02-09	1	-0/+55