Changeset 2911
- Timestamp:
- Mar 20, 2013, 12:12:28 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLabsToRTL.ma
r2866 r2911 448 448 bind_new register (list (joint_seq RTL globals)) ≝ 449 449 λglobals,src_sign,destrs,srcrs. 450 match reduce_strong ?? destrs srcrs with450 match reduce_strong ?? srcrs destrs with 451 451 [ mk_Sig t prf ⇒ 452 452 let src_common ≝ \fst (\fst t) in
Note: See TracChangeset
for help on using the changeset viewer.