diff options
Diffstat (limited to 'extraction/extraction.v')
| -rw-r--r-- | extraction/extraction.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index 247d6cfb..c5751e2b 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -76,6 +76,8 @@ Extraction Inline RTLgen.ret RTLgen.error RTLgen.bind RTLgen.bind2. (* Inlining *) Extract Inlined Constant Inlining.should_inline => "Inliningaux.should_inline". +Extract Inlined Constant Inlining.inlining_info => "Inliningaux.inlining_info". +Extract Inlined Constant Inlining.inlining_analysis => "Inliningaux.inlining_analysis". Extraction Inline Inlining.ret Inlining.bind. (* Allocation *) |