Ignore:
Timestamp:
Apr 7, 2011, 6:53:59 PM (9 years ago)
Author:
campbell
Message:

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r700 r744  
    424424  ].
    425425
    426 definition size_init_data : init_data → Z
     426definition size_init_data : init_data → nat
    427427 λi_data.match i_data with
    428428  [ Init_int8 _ ⇒ 1
     
    431431  | Init_float32 _ ⇒ 4
    432432  | Init_float64 _ ⇒ 8
    433   | Init_space n ⇒ Zmax n 0
     433  | Init_space n ⇒ max n 0
    434434  | Init_null r ⇒ size_pointer r
    435435  | Init_addrof r _ _ ⇒ size_pointer r].
Note: See TracChangeset for help on using the changeset viewer.