summaryrefslogtreecommitdiff
path: root/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'extraction')
-rw-r--r--extraction/extraction.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 52706ab..4861ff9 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -83,7 +83,6 @@ Extract Constant Compiler.print_Clight => "PrintClight.print_if".
Extract Constant Compiler.print_Cminor => "PrintCminor.print_if".
Extract Constant Compiler.print_RTL => "PrintRTL.print_rtl".
Extract Constant Compiler.print_RTL_tailcall => "PrintRTL.print_tailcall".
-Extract Constant Compiler.print_RTL_castopt => "PrintRTL.print_castopt".
Extract Constant Compiler.print_RTL_constprop => "PrintRTL.print_constprop".
Extract Constant Compiler.print_RTL_cse => "PrintRTL.print_cse".
Extract Constant Compiler.print_LTLin => "PrintLTLin.print_if".