Ignore:
Timestamp:
Feb 1, 2013, 12:13:22 PM (8 years ago)
Author:
garnier
Message:

Memory injections are now only defined relatively to block ids, not regions. Used to prove some more unfinished lemmas.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorOps.ma

    r2588 r2600  
    192192lapply H1 lapply H2 -H1 -H2
    193193whd in ⊢ ((??%?) → (??%?) → ?);
    194 cases (E b2) normalize nodelta
     194cases (E (block_id b2)) normalize nodelta
    195195[ #Habsurd destruct ]
    196196* #bx #ox normalize nodelta #Heq1 #Heq2 destruct
Note: See TracChangeset for help on using the changeset viewer.