Ignore:
Timestamp:
Feb 14, 2013, 11:49:48 AM (7 years ago)
Author:
piccolo
Message:

bug fixed in blocks.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL_semantics.ma

    r2604 r2666  
    114114   | ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st
    115115   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed. 
    116          
    117 definition ERTL_semantics ≝
    118   make_sem_graph_params ERTL
    119   (λF. mk_sem_unserialized_params ??
     116
     117definition ERTL_sem_uns ≝ 
     118λF. mk_sem_unserialized_params ERTL ?
    120119  (* st_pars            ≝ *) ERTL_state
    121120  (* acca_store_        ≝ *) ps_reg_store
     
    142141     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
    143142  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertl_seq F gl ge stm id)
    144   (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …)).
     143  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …).
     144         
     145definition ERTL_semantics ≝
     146  make_sem_graph_params ERTL ERTL_sem_uns.
Note: See TracChangeset for help on using the changeset viewer.