Ignore:
Timestamp:
Apr 4, 2012, 6:48:26 PM (8 years ago)
Author:
campbell
Message:

Update Cexec soundness proof.
Change finishes_with predicate to inductive form so that qed no longer
spends huge amounts of time typechecking.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r1713 r1876  
    349349[ #en #m #en' #m' #EXEC whd in EXEC:(??%?); destruct %
    350350| * #id #ty #t #IH #en #m #en' #m'
    351   lapply (refl ? (alloc m O (sizeof ty) Any)) #ALLOC #EXEC
     351  lapply (refl ? (alloc ? m O (sizeof ty) Any)) #ALLOC #EXEC
    352352  whd in EXEC:(??%?) ALLOC:(???%);
    353353 @(alloc_variables_cons … ALLOC)
Note: See TracChangeset for help on using the changeset viewer.