Changeset 2106


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

Fix up a couple of proofs broken by recent changes.

Location:
src/Clight
Files:
2 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
  • src/Clight/test/search.test.ma

    r1991 r2106  
    3838example fe : finishes_with (repr 3) state (
    3939bind ? (snapshot state) (front_end myprog) (λp.
    40 exec_up_to RTLabs_fullexec p 1000 [ ])).
     40exec_up_to RTLabs_fullexec (\snd p) 1000 [ ])).
    4141normalize
    4242%
Note: See TracChangeset for help on using the changeset viewer.