Changeset 790


Ignore:
Timestamp:
May 10, 2011, 5:50:09 PM (9 years ago)
Author:
campbell
Message:

A little tidying: get rid of requirement for jmeq in Mem.ma, remove extra case
in Cminor -> RTLabs.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r780 r790  
    320320    do f ← add_stmt env label_env s' exits ptrs f;
    321321    add_fresh_to_graph (St_cost l) f
    322 | _ ⇒ Error ? (* XXX implement *)
    323322].
    324323[ @(λ_. St_skip l_next)
  • src/common/Mem.ma

    r744 r790  
    128128  The following functions extract the size information from a chunk. *)
    129129
    130 definition size_chunk : memory_chunk → Z
     130definition size_chunk : memory_chunk → nat
    131131  λchunk.match chunk with
    132132  [ Mint8signed => 1
Note: See TracChangeset for help on using the changeset viewer.