Changeset 1254 for src/ERTL/ERTL.ma


Ignore:
Timestamp:
Sep 22, 2011, 4:16:06 PM (9 years ago)
Author:
sacerdot
Message:

More progress towards porting of RTLtoERTL to joint syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1252 r1254  
    77                 
    88inductive ertl_statement_extension: Type[0] ≝
    9   | ertl_st_ext_new_frame: label → ertl_statement_extension
    10   | ertl_st_ext_del_frame: label → ertl_statement_extension
    11   | ertl_st_ext_frame_size: register → label → ertl_statement_extension.
     9  | ertl_st_ext_new_frame: ertl_statement_extension
     10  | ertl_st_ext_del_frame: ertl_statement_extension
     11  | ertl_st_ext_frame_size: register → ertl_statement_extension.
    1212
    1313definition ertl_params_: params_ ≝
Note: See TracChangeset for help on using the changeset viewer.