Changeset 878 for src/RTLabs/import.ma

Timestamp:

Jun 3, 2011, 5:35:27 PM (9 years ago)

Author:

campbell

Message:

Removal of manually inserted record projections.

File:

• src/RTLabs/import.ma (modified) (1 diff)

src/RTLabs/import.ma

@@ -23 +23 @@
 ; pf_exit      : nat
 }.
-(* XXX projection generation with nat broken *)
-definition pf_stacksize ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ s _ _ _ ⇒ s ].
-definition pf_graph ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ g _ _ ⇒ g ].
-definition pf_entry ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ _ e _ ⇒ e ].
-definition pf_exit ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ _ _ e ⇒ e ].
 
 definition make_register :