Changeset 2912

Timestamp:

Mar 20, 2013, 12:21:43 AM (7 years ago)

Author:

sacerdot

Message:

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

File:

• src/RTLabs/RTLabsToRTL.ma (modified) (1 diff)

src/RTLabs/RTLabsToRTL.ma

@@ -455 +455 @@
     let dst_rest   ≝ \snd (\snd t) in
     (* first, move the common part *)
-    translate_move ? src_common (map … (Reg ?) dst_common) ? @@
+    translate_move ? dst_common (map … (Reg ?) src_common) ? @@
     match src_rest return λ_.bind_new ?? with
     [ nil ⇒ (* upcast *)