diff options
Diffstat (limited to 'extraction/extraction.v')
| -rw-r--r-- | extraction/extraction.v | 15 |
1 files changed, 3 insertions, 12 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index 265a5967..e4c1cb25 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -34,7 +34,6 @@ Require Clight. Require Compiler. Require Parser. Require Initializers. -Require Int31. Require Asmaux. (* Standard lib *) @@ -141,7 +140,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; @@ -150,15 +149,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. @@ -185,9 +175,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 |