Ignore:
Timestamp:
Feb 18, 2013, 5:48:19 PM (7 years ago)
Author:
tranquil
Message:
  • another change in block definition
  • RTLabs -> RTL and ERTL -> ERTLptr passes fixed, others stil broken
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL_semantics.ma

    r2666 r2674  
    142142  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertl_seq F gl ge stm id)
    143143  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …).
    144          
     144
    145145definition ERTL_semantics ≝
    146   make_sem_graph_params ERTL ERTL_sem_uns.
     146  mk_sem_graph_params ERTL ERTL_sem_uns.
Note: See TracChangeset for help on using the changeset viewer.