Ignore:
Timestamp:
Mar 21, 2013, 9:45:49 PM (5 years ago)
Author:
campbell
Message:

Disable initialisation code generation in Cminor, propogate init data
through RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r2924 r2936  
    939939qed.
    940940
    941 definition cminor_noinit_to_rtlabs : Cminor_noinit_program → RTLabs_program ≝
     941definition cminor_to_rtlabs : Cminor_program → RTLabs_program ≝
    942942λp.transform_program … p (λ_. transf_fundef … c2ra_function).
    943943
    944 include "Cminor/initialisation.ma".
    945 
    946 definition cminor_to_rtlabs : costlabel → Cminor_program → RTLabs_program ≝
    947 λinit_cost,p. let p' ≝ replace_init init_cost p in cminor_noinit_to_rtlabs p'.
Note: See TracChangeset for help on using the changeset viewer.