diff options
Diffstat (limited to 'extraction/extraction.v')
| -rw-r--r-- | extraction/extraction.v | 16 |
1 files changed, 4 insertions, 12 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index 15a64d89..521c0cdd 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -34,7 +34,6 @@ Require Clight. Require Compiler. Require Parser. Require Initializers. -Require Int31. (* Standard lib *) Require Import ExtrOcamlBasic. @@ -72,6 +71,7 @@ Extract Constant Iteration.GenIter.iterate => (* Selection *) Extract Constant Selection.compile_switch => "Switchaux.compile_switch". +Extract Constant Selection.if_conversion_heuristic => "Selectionaux.if_conversion_heuristic". (* RTLgen *) Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely". @@ -127,7 +127,7 @@ Extract Constant Compiler.time => "Timing.time_coq". (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) (* Cabs *) -Extract Constant Cabs.cabsloc => +Extract Constant Cabs.loc => "{ lineno : int; filename: string; byteno: int; @@ -136,15 +136,6 @@ Extract Constant Cabs.cabsloc => Extract Inlined Constant Cabs.string => "String.t". Extract Constant Cabs.char_code => "int64". -(* Int31 *) -Extract Inductive Int31.digits => "bool" [ "false" "true" ]. -Extract Inductive Int31.int31 => "int" [ "Camlcoq.Int31.constr" ] "Camlcoq.Int31.destr". -Extract Constant Int31.twice => "Camlcoq.Int31.twice". -Extract Constant Int31.twice_plus_one => "Camlcoq.Int31.twice_plus_one". -Extract Constant Int31.compare31 => "Camlcoq.Int31.compare". -Extract Constant Int31.On => "0". -Extract Constant Int31.In => "1". - (* Processor-specific extraction directives *) Load extractionMachdep. @@ -171,9 +162,10 @@ Separate Extraction Cexec.do_initial_state Cexec.do_step Cexec.at_final_state Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env Initializers.transl_init Initializers.constval - Csyntax.Eindex Csyntax.Epreincr + Csyntax.Eindex Csyntax.Epreincr Csyntax.Eselection Ctyping.typecheck_program Ctyping.epostincr Ctyping.epostdecr Ctyping.epreincr Ctyping.epredecr + Ctyping.eselection Ctypes.make_program Clight.type_of_function Conventions1.callee_save_type Conventions1.is_float_reg |