Changeset 878 for src/RTLabs/import.ma


Ignore:
Timestamp:
Jun 3, 2011, 5:35:27 PM (9 years ago)
Author:
campbell
Message:

Removal of manually inserted record projections.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/import.ma

    r816 r878  
    2323; pf_exit      : nat
    2424}.
    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 ].
    3025
    3126definition make_register :
Note: See TracChangeset for help on using the changeset viewer.