Changeset 2562 for src/joint/Traces.ma


Ignore:
Timestamp:
Dec 19, 2012, 10:38:43 AM (8 years ago)
Author:
piccolo
Message:

linearise modified

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2561 r2562  
    7979  (* use exit_pc as ra and call_dest_for_main as dest *)
    8080  let st0' ≝ mk_state_pc … (set_sp … spp st0) exit_pc exit_pc in
    81   ! st0_no_pc ← save_frame ?? sem_globals call_id (call_dest_for_main … pars) st0' ;
     81  ! st0_no_pc ← save_frame ?? sem_globals ID (call_dest_for_main … pars) st0' ;
    8282  let st0'' ≝ set_no_pc … st0_no_pc st0' in
    8383  ! bl ← block_of_call … ge (inl … main) st0'';
     
    160160    normalize nodelta ]
    161161  #ABS destruct(ABS) ]
    162 * [ #s | #f' #args #dest | #a #lbl ] #nxt #fetch >m_return_bind
     162* [ #f' #args #dest | #a #lbl | #s ] #nxt #fetch >m_return_bind
    163163normalize nodelta
    164 [1,3: normalize in ⊢ (%→?); #ABS destruct(ABS) ]
     164[2,3: normalize in ⊢ (%→?); #ABS destruct(ABS) ]
    165165whd in match joint_classify_step;
    166166normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.