diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-07-31 12:44:18 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-07-31 12:44:18 +0000 |
| commit | 4c8a550fae641115170e4fc9c1b1292834e0c6c0 (patch) | |
| tree | 2363194510dce61b3a6e3280601654c0c8646f9a /extraction/extraction.v | |
| parent | 99294ec7c8054b92536d14883599ff3bfe7745ee (diff) | |
Flag to turn on/off the recognition of fused multiply-add and multiply-sub
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@706 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'extraction/extraction.v')
| -rw-r--r-- | extraction/extraction.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index abb792c..69034bc 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -50,6 +50,9 @@ Extract Constant Iteration.GenIter.iterate => in iter". +(* Selection *) +Extract Constant Selection.use_fused_mul => "(fun () -> !Clflags.option_fmadd)". + (* RTLgen *) Extract Constant RTLgen.compile_switch => "RTLgenaux.compile_switch". Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely". |