Changeset 1372 for src/ERTL


Ignore:
Timestamp:
Oct 14, 2011, 2:48:34 PM (8 years ago)
Author:
sacerdot
Message:

save_frame now takes the stacksize to allow RTL to allocate the stack frame

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1371 r1372  
    5151     OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].
    5252
    53 definition ertl_save_frame: nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝
    54  λ_.λ_.λ_.λst.
     53definition ertl_save_frame: nat → nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝
     54 λ_.λ_.λ_.λ_.λst.
    5555  OK …
    5656   (set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st))
Note: See TracChangeset for help on using the changeset viewer.