Changeset 1315


Ignore:
Timestamp:
Oct 7, 2011, 11:12:34 AM (8 years ago)
Author:
mulligan
Message:

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

Location:
src
Files:
1 edited
1 moved

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r1314 r1315  
    179179  | Oaddrstack offset ⇒
    180180    let 〈r1, r2〉 ≝ make_addr … destrs ? in
    181       add_graph rtl_params1 globals start_lbl (sequential … (STACK_ADDRESS rtl_params_ globals r1 r2) dest_lbl) def
     181      ?
     182      (* add_graph rtl_params1 globals start_lbl (sequential … (STACK_ADDRESS rtl_params_ globals r1 r2) dest_lbl) def *)
    182183  ].
    183184  [1: >bytes_length_proof
     
    189190      ]
    190191  |5: cases not_implemented (* XXX: float, error_float in o'caml *)
    191   ].
     192  |*: cases daemon
     193  ].
     194qed.
    192195 
    193196definition translate_move_internal ≝
Note: See TracChangeset for help on using the changeset viewer.