Changeset 2041


Ignore:
Timestamp:
Jun 8, 2012, 11:21:55 PM (5 years ago)
Author:
sacerdot
Message:

Repaired: unified syntax for monads.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1451 r2041  
    110110      let st ≝ set_hwsp newsp st in
    111111      ! st ← next … (ertl_sem_params1 globals) l st ;
    112         ret ? 〈E0,st〉
     112        return 〈E0,st〉
    113113   | ertl_st_ext_del_frame ⇒
    114114      ! v ← framesize … ge st;
     
    117117      let st ≝ set_hwsp newsp st in
    118118      ! st ← next … (ertl_sem_params1 …) l st ;
    119         ret ? 〈E0,st〉
     119        return 〈E0,st〉
    120120   | ertl_st_ext_frame_size dst ⇒
    121121      ! v ← framesize … ge st;
    122122      ! st ← greg_store ertl_sem_params dst (BVByte (bitvector_of_nat … v)) st;
    123123      ! st ← next … (ertl_sem_params1 …) l st ;
    124         ret ? 〈E0, st〉
     124        return 〈E0, st〉
    125125   ].
    126126
Note: See TracChangeset for help on using the changeset viewer.