Changeset 1995 for src/RTLabs


Ignore:
Timestamp:
May 24, 2012, 7:18:35 PM (7 years ago)
Author:
campbell
Message:

Overall compiler definition; bits and pieces to
make everything happy(ish).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r1601 r1995  
    212212qed.
    213213
     214(* Type safety in RTLabs has broken this for the moment...
    214215let rec translate_cst
    215216  (globals: list ident) (cst: constant) (destrs: list register)
     
    12511252definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
    12521253 λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))).
     1254
     1255*)
     1256axiom rtlabs_to_rtl: RTLabs_program → rtl_program.
     1257
Note: See TracChangeset for help on using the changeset viewer.