Ignore:
Timestamp:
Jan 31, 2013, 5:15:49 PM (8 years ago)
Author:
tranquil
Message:
  • map_opt and map on positive maps are now clean (erase empty subtrees)
  • minor changes to blocks
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_blocks.ma

    r2595 r2599  
    5151    return 〈curr_id, curr_fn〉 →
    5252  let src ≝ point_of_pc p (pc … st) in
    53   (* disambiguation: select 3rd (step list in code) *)
    54   src ~❨b, l❩~> dst in joint_if_code … curr_fn →
     53  step_list_in_code … (joint_if_code … curr_fn) src b l dst →
    5554  All ? (no_cost_label …) b →
    5655  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
     
    138137    return 〈curr_id, curr_fn〉 →
    139138  let src ≝ point_of_pc p (pc … st) in
    140   (* disambiguation: select 3rd (step list in code) *)
    141   src ~❨b, l❩~> dst in joint_if_code … curr_fn →
     139  step_list_in_code … (joint_if_code … curr_fn) src b l dst →
    142140  All ? (no_cost_label …) b →
    143141  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
Note: See TracChangeset for help on using the changeset viewer.