debian-compcert - Debian packaging for CompCert

	Commit message (Collapse)	Author	Age
*	Remove some useless "Require".	xleroy	2012-12-30
\| \| \| \| \| \| \|	Update ARM port. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2085 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)	xleroy	2012-11-03
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2065 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Changelog: updated	xleroy	2012-06-28
\| \| \| \| \| \| \| \| \| \|	driver/Interp.ml: clean up dead code lib/Integers.v: add shifted_or_is_add lib/Floats.v: add from_words_eq .depend: updated git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1940 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Use Flocq for floats	xleroy	2012-06-28
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	float->int conversions, continued: weaker axiomatization.	xleroy	2010-10-29
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1545 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Float.intoffloat and Float.intuoffloat are now partial functions.	xleroy	2010-10-28
\| \| \| \| \| \| \|	(May fail if float is too big to be converted.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1544 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of the reuse-temps branch:	xleroy	2010-09-02
\| \| \| \| \| \| \| \| \| \| \| \|	- Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fewer float axioms.	xleroy	2010-05-09
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1343 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Suppressed axioms Float.eq_zero_{true,false}, since the latter is	xleroy	2010-05-09
\| \| \| \| \| \| \| \| \| \|	wrong because of +0.0 / -0.0. Adapted Clight semantics accordingly. (Truth value of a float is defined by comparison Float.cmp Ceq with 0.0, no longer by structural equality.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revised encoding/decoding of floats	xleroy	2010-05-09
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1341 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Adapted to work with Coq 8.2-1	xleroy	2009-06-05
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ↵	xleroy	2008-05-30
\| \| \| \| \| \|	utilisee dans le front-end C. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@647 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout license, README, copyright notices	xleroy	2008-01-27
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Petites adaptations pour Coq 8.1gamma	xleroy	2006-11-11
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@135 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fusion de la branche "traces":	xleroy	2006-09-04
\| \| \| \| \| \| \| \| \| \| \| \| \|	- Ajout de traces d'evenements d'E/S dans les semantiques - Ajout constructions switch et allocation dynamique - Initialisation des variables globales - Portage Coq 8.1 beta Debut d'integration du front-end C: - Traduction Clight -> Csharpminor dans cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Initial import of compcert	xleroy	2006-02-09
	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e