Ignore:
Timestamp:
May 24, 2012, 11:39:27 AM (7 years ago)
Author:
campbell
Message:

Abstraction of the memory contents in the memory models is no longer
necessary.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r1876 r1988  
    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.