Changeset 878 for src/RTLabs/syntax.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/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.