Changeset 190 for C-semantics

Timestamp:

Oct 18, 2010, 11:36:10 AM (9 years ago)

Author:

campbell

Message:

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

File:

• C-semantics/Mem.ma (modified) (6 diffs)

C-semantics/Mem.ma

@@ -1026 +1026 @@
 ncases (in_bounds m1 chunk' psp' b' ofs');
 ##[#Hvalid1;nrewrite > (in_bounds_true m2 chunk' psp' b' ofs' ? (Some ? ?) ??);
-   ##[nwhd in ⊢ (???%);napply eq_f;napply eq_f;
+   ##[nwhd in ⊢ (???%); napply (eq_f … (Some val));napply (eq_f … (load_result chunk'));
       nrewrite > Heq;nwhd in ⊢ (??(???(? (? % ?)))?);
                      nwhd in ⊢ (??(???(? %))?);
@@ -1086 +1086 @@
    napply (store_valid_access_1 … STORE);//
 ##|#H3;ncases H3;
-   #x;#Hx;nrewrite > Hx;napply eq_f;
+   #x;#Hx;nrewrite > Hx;napply (eq_f … (Some val));
    napply (load_store_overlap … STORE … Hx);//;##]
 nqed.
@@ -1123 +1123 @@
    napply
     (store_valid_access_1 … STORE);//
-##|*;#x;#Hx;nrewrite > Hx;napply eq_f;
+##|*;#x;#Hx;nrewrite > Hx;napply (eq_f … (Some val));
    napply (load_store_mismatch … STORE … Hsize);//;##]
 nqed.
@@ -1207 +1207 @@
      ##| nrewrite < H1 in ⊢ (% → ?);#Hx';
          nrewrite < H1 in Hx;#Hx;nrewrite > Hx;
-      napply eq_f;napply (load_store_overlap … STORE … Hx');/2/;
+      napply (eq_f … (Some val));napply (load_store_overlap … STORE … Hx');/2/;
      ##]
    ##|#H1;#H2;#H3;
@@ -1214 +1214 @@
            nrewrite > H1; nelim (store_valid_access_3 … STORE); //
        ##| nrewrite < H1 in Hx ⊢ %; nrewrite < H2; #Hx Hx';
-           nrewrite > Hx;napply eq_f;
+           nrewrite > Hx;napply (eq_f … (Some val));
            napply (load_store_mismatch … STORE … Hx');/2/
        ##]
@@ -1517 +1517 @@
   ##| nrewrite > (class_alloc_same … ALLOC); //
   ##]
-##| *; #v;#LOAD; nrewrite > LOAD; napply eq_f;
+##| *; #v;#LOAD; nrewrite > LOAD; napply (eq_f … (Some val));
     napply (load_alloc_same … ALLOC … LOAD);
 ##] nqed.