diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-01-20 18:13:58 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-01-20 18:13:58 +0100 |
commit | 12803784f2753863985d1030999469c18e01e0f1 (patch) | |
tree | 8d57c675f5d9ac36539ece743710e82b6b06fa9c /extraction | |
parent | 07e482340977d1ee469eed81d0dae25d49e5abe8 (diff) | |
parent | fe7da33a1992c3023a2e7e3f36c532ad10e3f236 (diff) | |
download | compcert-12803784f2753863985d1030999469c18e01e0f1.tar.gz compcert-12803784f2753863985d1030999469c18e01e0f1.zip |
Merge branch 'master' into dwarf
Diffstat (limited to 'extraction')
-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 ee496ffa..94ac6f52 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -57,12 +57,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 *) |