diff options
Diffstat (limited to 'extraction/extraction.v')
-rw-r--r-- | extraction/extraction.v | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index 45239aa5..1db52ef3 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -60,12 +60,6 @@ Extract Constant Iteration.GenIter.iterate => (* Selection *) -Extract Constant SelectLong.get_helper => - "fun ge s sg -> - Errors.OK (Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s))". -Extract Constant SelectLong.get_builtin => - "fun s sg -> - Errors.OK (Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s))". Extract Constant Selection.compile_switch => "Switchaux.compile_switch". (* RTLgen *) |