aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'extraction')
-rw-r--r--extraction/extraction.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 15a64d89..c0286f7b 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -72,6 +72,7 @@ Extract Constant Iteration.GenIter.iterate =>
(* Selection *)
Extract Constant Selection.compile_switch => "Switchaux.compile_switch".
+Extract Constant Selection.if_conversion_heuristic => "Selectionaux.if_conversion_heuristic".
(* RTLgen *)
Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely".