From 265fa07b34a813ba9d8249ddad82d71e6002c10d Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 2 Sep 2010 12:42:19 +0000 Subject: Merge of the reuse-temps branch: - 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 --- extraction/extraction.v | 1 - 1 file changed, 1 deletion(-) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index 706d1db..8e3c1aa 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -28,7 +28,6 @@ Extract Inductive List.list => "list" [ "[]" "(::)" ]. (* Float *) Extract Inlined Constant Floats.float => "float". Extract Constant Floats.Float.zero => "0.". -Extract Constant Floats.Float.one => "1.". Extract Constant Floats.Float.neg => "( ~-. )". Extract Constant Floats.Float.abs => "abs_float". Extract Constant Floats.Float.singleoffloat => "Floataux.singleoffloat". -- cgit v1.2.3