Changeset 2035


Ignore:
Timestamp:
Jun 8, 2012, 5:51:35 PM (5 years ago)
Author:
sacerdot
Message:

Fixed

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLToERTL.ma

    r2032 r2035  
    246246  λglobals,params.
    247247  let n ≝ min (|params|) (|RegisterParams|) in
    248   let hdw_stack_params ≝ vsplit ? params n ? in
     248  let hdw_stack_params ≝ split ? params n in
    249249  let hdw_params ≝ \fst hdw_stack_params in
    250250  let stack_params ≝ \snd hdw_stack_params in
    251251    set_params_hdw globals hdw_params @ set_params_stack globals stack_params.
    252 normalize nodelta /2/
    253 qed.
    254252
    255253definition fetch_result ≝
Note: See TracChangeset for help on using the changeset viewer.