Ignore:
Timestamp:
May 24, 2012, 11:39:27 AM (7 years ago)
Author:
campbell
Message:

Abstraction of the memory contents in the memory models is no longer
necessary.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEGlobalenvs.ma

    r1599 r1988  
    428428  λm,i_data,r.
    429429  let b ≝ mk_block r (nextblock … m) in
    430   〈mk_mem ? (update_block ? b
    431                  (mk_block_contents (mk_contentT beval BVundef) OZ i_data (λ_.BVundef))
     430  〈mk_mem (update_block ? b
     431                 (mk_block_contents OZ i_data (λ_.BVundef))
    432432                 (blocks … m))
    433433         (Zsucc (nextblock … m))
Note: See TracChangeset for help on using the changeset viewer.