Changeset 2488


Ignore:
Timestamp:
Nov 23, 2012, 4:29:34 PM (7 years ago)
Author:
garnier
Message:

glitch fixed

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2487 r2488  
    32673267       [ 1: cases sss_incl // ] * * #Hvalid #Hlow #Hhigh
    32683268       lapply (store_int_success … i … Hvalid Hlow Hhigh) * #m_ext' #Hstore
    3269        lapply (store_value_load_value_ok … Hstore) // #Hload_value_correct
     3269       lapply (store_value_load_value_compatible … Hstore) // #Hload_value_correct
    32703270       >Hstore whd in match (m_bind ?????); whd @conj try //
    32713271       cut (mem block res sss_writeable)
Note: See TracChangeset for help on using the changeset viewer.