Changeset 2862

Timestamp:

Mar 13, 2013, 2:07:20 PM (8 years ago)

Author:

sacerdot

Message:

Repaired, a reverse was enough.

File:

• src/RTL/RTLToERTL.ma (modified) (2 diffs)

src/RTL/RTLToERTL.ma

@@ -301 +301 @@
     (* init_stack_size ≝ *) new_stacksize
     (* added_prologue ≝ *) prologue
-    (* new_regs ≝ *) (addr2 :: addr1 :: tmpr :: rah :: ral :: map … (λx.\fst x) to_save)
+    (* new_regs ≝ *) (reverse … (addr2 :: addr1 :: tmpr :: rah :: ral :: map … (λx.\fst x) to_save))
     (* f_step ≝ *) (translate_step globals)
     (* f_fin ≝ *) (translate_fin_step globals (joint_if_result … def) ral rah to_save)
@@ -313 +313 @@
   try #a try #b try #c try #d try #e try #f destruct
   cases a in b; #a1 #a2 normalize nodelta #EQ destruct
-| #r1 #r2 #r3 #r4 #r5 #r6 #r7 #r8 #ral #rah #tmpr #addr1 #addr2 
-change with (? = ?)
+| #r1 #r2 #r3 #r4 #r5 #r6 #r7 #r8 #ral #rah #tmpr #addr1 #addr2
 % (* XXX: FAILS, unintentional list reversal??? *)
 ]