Changeset 1995 for src/RTLabs/RTLabsToRTL.ma

Timestamp:

May 24, 2012, 7:18:35 PM (8 years ago)

Author:

campbell

Message:

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

File:

• src/RTLabs/RTLabsToRTL.ma (modified) (2 diffs)

src/RTLabs/RTLabsToRTL.ma

@@ -212 +212 @@
 qed.
 
+(* Type safety in RTLabs has broken this for the moment...
 let rec translate_cst
   (globals: list ident) (cst: constant) (destrs: list register)
@@ -1251 +1252 @@
 definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
  λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))).
+
+*)
+axiom rtlabs_to_rtl: RTLabs_program → rtl_program.
+