Changeset 961 for src/common/Globalenvs.ma
- Timestamp:
- Jun 15, 2011, 4:15:52 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Globalenvs.ma
r797 r961 406 406 let r ≝ block_region m b in 407 407 match id with 408 [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint n)409 | Init_int16 n ⇒ store Mint16unsigned m r b p (Vint n)410 | Init_int32 n ⇒ store Mint32 m r b p (Vint n)408 [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint I8 n) 409 | Init_int16 n ⇒ store Mint16unsigned m r b p (Vint I16 n) 410 | Init_int32 n ⇒ store Mint32 m r b p (Vint I32 n) 411 411 | Init_float32 n ⇒ store Mfloat32 m r b p (Vfloat n) 412 412 | Init_float64 n ⇒ store Mfloat64 m r b p (Vfloat n) … … 416 416 | Some b' ⇒ 417 417 match pointer_compat_dec b' r' with 418 [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc (shift_offset zero_offset ofs))418 [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc (shift_offset ? zero_offset (repr I16 ofs))) 419 419 | inr _ ⇒ None ? 420 420 ]
Note: See TracChangeset
for help on using the changeset viewer.