Changeset 1178


Ignore:
Timestamp:
Sep 5, 2011, 11:26:06 AM (8 years ago)
Author:
mulligan
Message:

fixed ertl.ma to use new version of joint params

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1175 r1178  
    1212  | pseudo: register → move_registers
    1313  | hardware: Register → move_registers.
    14 
    15 definition ertl_params: params ≝
    16  mk_params register register register register (move_registers × move_registers) register.
    1714                 
    1815inductive ertl_statement_extension: Type[0] ≝
     
    2118  | ertl_st_ext_frame_size: register → label → ertl_statement_extension.
    2219
    23 definition ertl_statement ≝ joint_statement label ertl_statement_extension ertl_params.
     20definition ertl_params: params ≝
     21 mk_params
     22   label register register register register
     23     (move_registers × move_registers) register
     24       ertl_statement_extension unit (list register) nat.
     25
     26definition ertl_statement ≝ joint_statement ertl_params.
    2427
    2528definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals).
Note: See TracChangeset for help on using the changeset viewer.