diff --git a/extraction/extraction.v b/extraction/extraction.v index 137ddb06a00c372050137d2691b28be915f156a5..4eb107bb8d20d02a97e19a87af8a7c418c9e072b 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -54,7 +54,7 @@ Extract Constant Iteration.GenIter.iterate => (* Selection *) -Extract Constant Selection.use_fused_mul => "(fun () -> !Clflags.option_fmadd)". +Extract Constant SelectOp.use_fused_mul => "(fun () -> !Clflags.option_fmadd)". (* RTLgen *) Extract Constant RTLgen.compile_switch => "RTLgenaux.compile_switch".