Changeset 1995 for src/RTLabs/RTLabsToRTL.ma
- Timestamp:
- May 24, 2012, 7:18:35 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLabsToRTL.ma
r1601 r1995 212 212 qed. 213 213 214 (* Type safety in RTLabs has broken this for the moment... 214 215 let rec translate_cst 215 216 (globals: list ident) (cst: constant) (destrs: list register) … … 1251 1252 definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝ 1252 1253 λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))). 1254 1255 *) 1256 axiom rtlabs_to_rtl: RTLabs_program → rtl_program. 1257
Note: See TracChangeset
for help on using the changeset viewer.