Changeset 2975 for src/RTL/RTL.ma


Ignore:
Timestamp:
Mar 27, 2013, 4:07:02 PM (6 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/RTL/RTL.ma

    r2955 r2975  
    113113  res in
    114114let res ≝ add_graph … l2
    115   (sequential … (CALL RTL ? (inl … (prog_main … p)) [ ] [ ]) l3)
     115  (sequential … (CALL RTL ? (inl … (prog_main … p)) [ ] rs) l3)
    116116  res in
    117117let res ≝ add_graph … l3
     
    128128| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I}
    129129| ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); //
    130 | ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct @I
     130| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct try @I
     131  try % try % try % try % try % whd /2 by double_lt3/
    131132| %{l2} %{(init_cost_label … p)} %
    132133]
Note: See TracChangeset for help on using the changeset viewer.