Changeset 878 for src/Cminor


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

Removal of manually inserted record projections.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/syntax.ma

    r816 r878  
    3939; f_body      : stmt
    4040}.
    41 (* XXX: matita interpretations bug workaround *)
    42 definition f_stacksize : internal_function → nat ≝
    43 λf.match f with [ mk_internal_function _ _ _ _ s _ ⇒ s ].
    4441
    4542definition Cminor_program ≝ program (fundef internal_function) unit.
Note: See TracChangeset for help on using the changeset viewer.