Ignore:
Timestamp:
Feb 7, 2013, 2:15:51 PM (7 years ago)
Author:
piccolo
Message:

Back-end fixes for last Garnier's commit that removes the regions from
the blocks. Only part of the back-end has been fixed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/joint_semantics.ma

    r2601 r2638  
    7575(* special program counter that is guaranteed to not correspond to anything *)
    7676definition exit_pc : program_counter ≝
    77   mk_program_counter «mk_block Code (-1), refl …» one.
     77  mk_program_counter «mk_block (-1), refl …» one.
    7878
    7979definition null_pc : Pos →  program_counter ≝ λpos.
    80     mk_program_counter «mk_block Code OZ, refl …» pos.
     80    mk_program_counter «mk_block ?, ?» pos.
     81cases daemon qed.
    8182
    8283definition set_m: ∀p. bemem → state p → state p ≝
     
    161162  fetch_internal_function … (globalenv (λvars.fundef (F vars)) V i p)
    162163    bl = Error … [MSG BadFunction].
    163  #F#V#i#p ** #r #id #EQ1 #EQ2 destruct
     164 #F#V#i#p ** #r #id #EQ1 destruct
    164165 whd in match fetch_internal_function;
    165166  whd in match fetch_function; normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.