Changeset 190


Ignore:
Timestamp:
Oct 18, 2010, 11:36:10 AM (9 years ago)
Author:
campbell
Message:

Minor changes to work with current matita HEAD (r10998).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Mem.ma

    r156 r190  
    10261026ncases (in_bounds m1 chunk' psp' b' ofs');
    10271027##[#Hvalid1;nrewrite > (in_bounds_true m2 chunk' psp' b' ofs' ? (Some ? ?) ??);
    1028    ##[nwhd in ⊢ (???%);napply eq_f;napply eq_f;
     1028   ##[nwhd in ⊢ (???%); napply (eq_f … (Some val));napply (eq_f … (load_result chunk'));
    10291029      nrewrite > Heq;nwhd in ⊢ (??(???(? (? % ?)))?);
    10301030                     nwhd in ⊢ (??(???(? %))?);
     
    10861086   napply (store_valid_access_1 … STORE);//
    10871087##|#H3;ncases H3;
    1088    #x;#Hx;nrewrite > Hx;napply eq_f;
     1088   #x;#Hx;nrewrite > Hx;napply (eq_f … (Some val));
    10891089   napply (load_store_overlap … STORE … Hx);//;##]
    10901090nqed.
     
    11231123   napply
    11241124    (store_valid_access_1 … STORE);//
    1125 ##|*;#x;#Hx;nrewrite > Hx;napply eq_f;
     1125##|*;#x;#Hx;nrewrite > Hx;napply (eq_f … (Some val));
    11261126   napply (load_store_mismatch … STORE … Hsize);//;##]
    11271127nqed.
     
    12071207     ##| nrewrite < H1 in ⊢ (% → ?);#Hx';
    12081208         nrewrite < H1 in Hx;#Hx;nrewrite > Hx;
    1209       napply eq_f;napply (load_store_overlap … STORE … Hx');/2/;
     1209      napply (eq_f … (Some val));napply (load_store_overlap … STORE … Hx');/2/;
    12101210     ##]
    12111211   ##|#H1;#H2;#H3;
     
    12141214           nrewrite > H1; nelim (store_valid_access_3 … STORE); //
    12151215       ##| nrewrite < H1 in Hx ⊢ %; nrewrite < H2; #Hx Hx';
    1216            nrewrite > Hx;napply eq_f;
     1216           nrewrite > Hx;napply (eq_f … (Some val));
    12171217           napply (load_store_mismatch … STORE … Hx');/2/
    12181218       ##]
     
    15171517  ##| nrewrite > (class_alloc_same … ALLOC); //
    15181518  ##]
    1519 ##| *; #v;#LOAD; nrewrite > LOAD; napply eq_f;
     1519##| *; #v;#LOAD; nrewrite > LOAD; napply (eq_f … (Some val));
    15201520    napply (load_alloc_same … ALLOC … LOAD);
    15211521##] nqed.
Note: See TracChangeset for help on using the changeset viewer.