Ignore:
Timestamp:
Feb 11, 2011, 4:45:28 PM (9 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/CexecComplete.ma

    r487 r496  
    4040
    4141lemma is_pointer_compat_true: ∀m,b,sp.
    42   pointer_compat (block_space m b) sp →
    43   is_pointer_compat (block_space m b) sp = true.
     42  pointer_compat (block_region m b) sp →
     43  is_pointer_compat (block_region m b) sp = true.
    4444#m #b #sp #H whd in ⊢ (??%?);
    45 elim (pointer_compat_dec (block_space m b) sp);
     45elim (pointer_compat_dec (block_region m b) sp);
    4646[ //
    4747| #H' @False_ind @(absurd … H H')
Note: See TracChangeset for help on using the changeset viewer.