diff options
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index e7f2e2fc..8e13264c 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -12,6 +12,7 @@ Require Coqlib. Require Wfsimpl. +Require DecidableClass Decidableplus. Require AST. Require Iteration. Require Floats. @@ -39,6 +40,12 @@ Require Import ExtrOcamlString. (* Coqlib *) Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)". +(* Decidable *) + +Extraction Inline DecidableClass.Decidable_witness DecidableClass.decide + Decidableplus.Decidable_and Decidableplus.Decidable_or + Decidableplus.Decidable_not Decidableplus.Decidable_implies. + (* Wfsimpl *) Extraction Inline Wfsimpl.Fix Wfsimpl.Fixm. @@ -159,12 +166,13 @@ Separate Extraction Ctyping.typecheck_program Ctyping.epostincr Ctyping.epostdecr Ctyping.epreincr Ctyping.epredecr Ctypes.make_program - Conventions1.int_caller_save_regs Conventions1.float_caller_save_regs - Conventions1.int_callee_save_regs Conventions1.float_callee_save_regs + Conventions1.int_caller_save_regs Conventions1.float_caller_save_regs + Conventions1.int_callee_save_regs Conventions1.float_callee_save_regs Conventions1.dummy_int_reg Conventions1.dummy_float_reg RTL.instr_defs RTL.instr_uses Machregs.mregs_for_operation Machregs.mregs_for_builtin Machregs.two_address_op Machregs.is_stack_reg + Machregs.destroyed_at_indirect_call AST.signature_main Floats.Float32.from_parsed Floats.Float.from_parsed Globalenvs.Senv.invert_symbol |