diff options
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index b9f684e..344a00f 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -21,6 +21,7 @@ Require Inlining. Require ValueDomain. Require Tailcall. Require Allocation. +Require Ctypes. Require Compiler. (* Standard lib *) @@ -125,6 +126,7 @@ Cd "extraction". 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 Initializers.transl_init Initializers.constval Csyntax.Eindex Csyntax.Epreincr Conventions1.dummy_int_reg Conventions1.dummy_float_reg |