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

pointer_compat is a little more natural if it takes that block rather than
the block's region.

File:
1 edited

Legend:

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

    r498 r499  
    102102            #e <e
    103103            whd in match (is_pointer_compat ??) in e''';
    104             cases (pointer_compat_dec (block_region m b) s') in e'''; #Hcompat #e'''
     104            cases (pointer_compat_dec b s') in e'''; #Hcompat #e'''
    105105            whd in e''':(??%?); destruct (e'''); /2/
    106106        ]
Note: See TracChangeset for help on using the changeset viewer.