Ignore:
Timestamp:
Feb 11, 2011, 4:45:28 PM (8 years ago)
Author:
campbell
Message:

First pass at moving regions to block type.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/CexecSound.ma

    r487 r496  
    102102            #e <e
    103103            whd in match (is_pointer_compat ??) in e''';
    104             cases (pointer_compat_dec (block_space m b) s') in e'''; #Hcompat #e'''
     104            cases (pointer_compat_dec (block_region m b) s') in e'''; #Hcompat #e'''
    105105            whd in e''':(??%?); destruct (e'''); /2/
    106106        ]
     
    514514@bind_OK #m #Em
    515515@opt_bind_OK #x cases x; #sp #b #esb
    516 @opt_bind_OK #u #ecode
    517516@opt_bind_OK #f #ef
    518 cases sp in esb ecode; #esb #ecode whd in ecode:(??%%); [ 1,2,3,4,5: destruct (ecode); ]
    519517whd; % [ whd in ⊢ (???(??%)) // | @(initial_state_intro … Ege Em esb ef) ]
    520518qed.
Note: See TracChangeset for help on using the changeset viewer.