Changeset 2912


Ignore:
Timestamp:
Mar 20, 2013, 12:21:43 AM (4 years ago)
Author:
sacerdot
Message:

Ouch, another bug in the very same function.
Fixed too, on an example everything works well now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r2911 r2912  
    455455    let dst_rest   ≝ \snd (\snd t) in
    456456    (* first, move the common part *)
    457     translate_move ? src_common (map … (Reg ?) dst_common) ? @@
     457    translate_move ? dst_common (map … (Reg ?) src_common) ? @@
    458458    match src_rest return λ_.bind_new ?? with
    459459    [ nil ⇒ (* upcast *)
Note: See TracChangeset for help on using the changeset viewer.