Changeset 878 for src/RTLabs

Timestamp:

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

Author:

campbell

Message:

Removal of manually inserted record projections.

Location:

src/RTLabs

Files:

• import.ma (modified) (1 diff)
• syntax.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 : 

src/RTLabs/syntax.ma

@@ -70 +70 @@
 ; f_exit      : label
 }.
-(* XXX: matita interpretations bug workaround *)
-definition f_stacksize : internal_function → nat ≝
-λf.match f with [ mk_internal_function _ _ _ _ _ _ _ s _ _  _ ⇒ s ].
 
 (* Note that the global variables will be initialised by the code in main