Changeset 878 for src/RTLabs/import.ma
- Timestamp:
- Jun 3, 2011, 5:35:27 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/import.ma
r816 r878 23 23 ; pf_exit : nat 24 24 }. 25 (* XXX projection generation with nat broken *)26 definition pf_stacksize ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ s _ _ _ ⇒ s ].27 definition pf_graph ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ g _ _ ⇒ g ].28 definition pf_entry ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ _ e _ ⇒ e ].29 definition pf_exit ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ _ _ e ⇒ e ].30 25 31 26 definition make_register :
Note: See TracChangeset
for help on using the changeset viewer.