Changeset 2955


Ignore:
Timestamp:
Mar 26, 2013, 4:11:12 PM (4 years ago)
Author:
tranquil
Message:

corrected stupid typo

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r2952 r2955  
    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)) [ ] [ ]) 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 try @I
    131   % try % try % try % try % try % try % try % try %
    132   whd whd in ⊢ (?%%); /2 by double_lt3/
     130| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct @I
    133131| %{l2} %{(init_cost_label … p)} %
    134132]
Note: See TracChangeset for help on using the changeset viewer.