Ignore:
Timestamp:
Jun 21, 2012, 5:21:05 PM (7 years ago)
Author:
campbell
Message:

Fix up a couple of proofs broken by recent changes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r2019 r2106  
    284284[ #en #m #en' #m' #EXEC whd in EXEC:(??%?); destruct %
    285285| * #id #ty #t #IH #en #m #en' #m'
    286   lapply (refl ? (alloc m O (sizeof ty) Any)) #ALLOC #EXEC
    287   whd in EXEC:(??%?) ALLOC:(???%);
     286  lapply (refl ? (alloc m O (sizeof ty) Any)) whd in ⊢ (? → ??%? → ?);
     287  cases (alloc ????) in ⊢ (???% → %); #m'' #b #ALLOC #EXEC
    288288 @(alloc_variables_cons … ALLOC)
    289289 @IH @EXEC
Note: See TracChangeset for help on using the changeset viewer.