Changeset 2103 for src/RTLabs


Ignore:
Timestamp:
Jun 21, 2012, 5:21:02 PM (7 years ago)
Author:
campbell
Message:

Make transform_*program take a more general transformation to make
properties easier to state.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r2032 r2103  
    12511251  because of CompCert heritage *)
    12521252definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
    1253  λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))).
     1253 λp. transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).
    12541254
    12551255*)
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r2032 r2103  
    951951  because of CompCert heritage *)
    952952definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
    953  λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))).
     953 λp. transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).
Note: See TracChangeset for help on using the changeset viewer.