Changeset 2975 for src/common


Ignore:
Timestamp:
Mar 27, 2013, 4:07:02 PM (7 years ago)
Author:
tranquil
Message:
  • RTL premain fixed
  • fixed bug in back end ops (subtracting to a porinter was reversed)
  • fixed globals initialization in LINToASM
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/BackEndOps.ma

    r2926 r2975  
    151151        else
    152152          let o1o0 : Byte × Byte ≝ vsplit ? 8 8 (offv (poff ptr)) in
    153           let 〈rslt,carry〉 ≝ op2 eval false op b2 (\snd o1o0) in
     153          let 〈rslt,carry〉 ≝ op2 eval false op (\snd o1o0) b2 in
    154154          let p0 ≝ mk_part 0 (le_S … (le_n …)) in
    155155          let ptr' ≝ mk_pointer (pblock ptr) (mk_offset (\fst o1o0 @@ rslt)) in
Note: See TracChangeset for help on using the changeset viewer.