diff options
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index f7e99545..ecd2853a 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -156,11 +156,11 @@ Separate Extraction Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env - Csyntax.make_program Clight.make_program Initializers.transl_init Initializers.constval Csyntax.Eindex Csyntax.Epreincr - Ctyping.retype_function Ctyping.econdition' + Ctyping.typecheck_program Ctyping.epostincr Ctyping.epostdecr Ctyping.epreincr Ctyping.epredecr + Clight.make_program Conventions1.dummy_int_reg Conventions1.dummy_float_reg RTL.instr_defs RTL.instr_uses Machregs.mregs_for_operation Machregs.mregs_for_builtin |