aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'extraction')
-rw-r--r--extraction/extraction.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 1bb5a709..b102503b 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -87,6 +87,9 @@ Extract Inlined Constant Inlining.inlining_info => "Inliningaux.inlining_info".
Extract Inlined Constant Inlining.inlining_analysis => "Inliningaux.inlining_analysis".
Extraction Inline Inlining.ret Inlining.bind.
+(* Loop invariant code motion *)
+Extract Inlined Constant LICM.gen_injections => "LICMaux.gen_injections".
+
(* Allocation *)
Extract Constant Allocation.regalloc => "Regalloc.regalloc".