Changeset 2912
- Timestamp:
- Mar 20, 2013, 12:21:43 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLabsToRTL.ma
r2911 r2912 455 455 let dst_rest ≝ \snd (\snd t) in 456 456 (* first, move the common part *) 457 translate_move ? src_common (map … (Reg ?) dst_common) ? @@457 translate_move ? dst_common (map … (Reg ?) src_common) ? @@ 458 458 match src_rest return λ_.bind_new ?? with 459 459 [ nil ⇒ (* upcast *)
Note: See TracChangeset
for help on using the changeset viewer.