Changeset 744 for src/RTLabs


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/RTLabs/RTLabs-sem.ma

    r736 r744  
    182182      match v with
    183183      [ Vint i ⇒
    184           ! l ← nth_opt ? (abs (unsigned i)) ls;
     184          ! l ← nth_opt ? (nat_of_bitvector ? i) ls;
    185185          ret ? 〈E0, build_state f fs m l〉
    186186      | _ ⇒ Wrong ???
Note: See TracChangeset for help on using the changeset viewer.