Changeset 790 for src/common


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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.