Changeset 1315 for src

Timestamp:

Oct 7, 2011, 11:12:34 AM (9 years ago)

Author:

mulligan

Message:

another move for the same reason. got rtlabs > rtl compiling again by using a daemon

Location:

src

Files:

• RTL/RTLToERTL.ma (moved) (moved from src/RTL/RTLtoERTL.ma)
• RTLabs/RTLabsToRTL.ma (modified) (2 diffs)

src/RTLabs/RTLabsToRTL.ma

@@ -179 +179 @@
   | Oaddrstack offset ⇒
     let 〈r1, r2〉 ≝ make_addr … destrs ? in
-      add_graph rtl_params1 globals start_lbl (sequential … (STACK_ADDRESS rtl_params_ globals r1 r2) dest_lbl) def
+      ?
+      (* add_graph rtl_params1 globals start_lbl (sequential … (STACK_ADDRESS rtl_params_ globals r1 r2) dest_lbl) def *)
   ].
   [1: >bytes_length_proof
@@ -189 +190 @@
       ]
   |5: cases not_implemented (* XXX: float, error_float in o'caml *)
-  ].
+  |*: cases daemon
+  ].
+qed.
   
 definition translate_move_internal ≝