Changeset 878 for src/RTL


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/RTL/RTL.ma

    r783 r878  
    4444}.
    4545
    46 definition rtl_if_stacksize: rtl_internal_function → nat.
    47   # R
    48   cases R
    49   # H1 # H2 # H3 # H4 # H5 # H6 # H7 # H8 # H9 # H10
    50   @ H7
    51 qed.
    5246
    5347inductive rtl_function_definition: Type[0] ≝
     
    6155  rtl_pr_main: option ident
    6256}.
    63 
    64 definition rtl_pr_vars: rtl_program → list (ident × nat).
    65   # P
    66   cases P
    67   # H1 # H2 # H3
    68   @ H1
    69 qed.
Note: See TracChangeset for help on using the changeset viewer.