Changeset 2931


Ignore:
Timestamp:
Mar 21, 2013, 7:31:23 PM (4 years ago)
Author:
sacerdot
Message:

Partial back-track from Paolo's commit, that was partial.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r2925 r2931  
    10931093(*CSC: here we are not doing any alignment on variables, like it is done in OCaml
    10941094  because of CompCert heritage *)
    1095 definition rtlabs_to_rtl: RTLabs_program → costlabel → rtl_program ≝
    1096  λp,init_cost.
    1097   mk_joint_program RTL
    1098     (transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)))
    1099     init_cost.
     1095definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
     1096 λp. transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).
Note: See TracChangeset for help on using the changeset viewer.