Changeset 878 for src/RTLabs


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

Removal of manually inserted record projections.

Location:
src/RTLabs
Files:
2 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 :
  • src/RTLabs/syntax.ma

    r816 r878  
    7070; f_exit      : label
    7171}.
    72 (* XXX: matita interpretations bug workaround *)
    73 definition f_stacksize : internal_function → nat ≝
    74 λf.match f with [ mk_internal_function _ _ _ _ _ _ _ s _ _  _ ⇒ s ].
    7572
    7673(* Note that the global variables will be initialised by the code in main
Note: See TracChangeset for help on using the changeset viewer.