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/ERTLptr/ERTLptr_semantics.ma

    r2604 r2666  
    2626                        ps_reg_store_status r addrh st
    2727   ].
    28    
    29 definition ERTLptr_semantics ≝
    30   make_sem_graph_params ERTLptr
    31   (λF. mk_sem_unserialized_params ??
     28
     29definition ERTLptr_sem_uns ≝
     30λF. mk_sem_unserialized_params ERTLptr ?
    3231  (* st_pars            ≝ *) ERTL_state
    3332  (* acca_store_        ≝ *) ps_reg_store
     
    5453     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
    5554  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertlptr_seq F gl ge stm id)
    56   (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …)).
     55  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …).
     56definition ERTLptr_semantics ≝
     57  make_sem_graph_params ERTLptr ERTLptr_sem_uns.
Note: See TracChangeset for help on using the changeset viewer.