Changeset 758 for src/common


Ignore:
Timestamp:
Apr 18, 2011, 12:33:35 PM (9 years ago)
Author:
campbell
Message:

Implement replacement of global var initialisation data by code in Cminor.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r747 r758  
    447447  ].
    448448
    449 definition size_init_data_list : list init_data → Z
    450   λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) OZ i_data.
     449definition size_init_data_list : list init_data → nat
     450  λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) O i_data.
    451451
    452452(* Nonessential properties that may require arithmetic
Note: See TracChangeset for help on using the changeset viewer.