Changeset 389 for C-semantics/CexecIO.ma


Ignore:
Timestamp:
Dec 8, 2010, 12:18:35 PM (9 years ago)
Author:
campbell
Message:

Sort out minor inconsistency between semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r388 r389  
    10011001  [ Kcall r f e k' ⇒
    10021002    match r with
    1003     [ None ⇒
    1004       match res with
    1005       [ Vundef ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
    1006       | _ ⇒ Wrong ???
    1007       ]
     1003    [ None ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
    10081004    | Some r' ⇒
    10091005      match r' with [ mk_pair l ty ⇒
     
    11451141##| #v k' m'; nwhd in ⊢ (?????%); ncases k'; //;
    11461142    #r f e k; nwhd in ⊢ (?????%); ncases r;
    1147   ##[ ncases v; nwhd; //;
     1143  ##[ nwhd; //;
    11481144  ##| #x; ncases x; #y; ncases y; #z; ncases z; #pcl b ofs ty;
    11491145    napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; nwhd in em':(??%?); //;
Note: See TracChangeset for help on using the changeset viewer.