From ed7f2503ea1b33fadb8f6aa5a538473ef3c58cab Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 25 Jan 2010 12:47:40 +0000 Subject: Updated ARM port git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1232 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- extraction/extraction.v | 4 ---- 1 file changed, 4 deletions(-) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index 77c6c62..6488d8b 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -52,10 +52,6 @@ Extract Constant Iteration.GenIter.iterate => match f a with Coq_inl b -> Some b | Coq_inr a' -> iter f a' in iter". - -(* Selection *) -Extract Constant SelectOp.use_fused_mul => "(fun () -> !Clflags.option_fmadd)". - (* RTLgen *) Extract Constant RTLgen.compile_switch => "RTLgenaux.compile_switch". Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely". -- cgit v1.2.3