Changeset 2862


Ignore:
Timestamp:
Mar 13, 2013, 2:07:20 PM (4 years ago)
Author:
sacerdot
Message:

Repaired, a reverse was enough.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLToERTL.ma

    r2861 r2862  
    301301    (* init_stack_size ≝ *) new_stacksize
    302302    (* added_prologue ≝ *) prologue
    303     (* new_regs ≝ *) (addr2 :: addr1 :: tmpr :: rah :: ral :: map … (λx.\fst x) to_save)
     303    (* new_regs ≝ *) (reverse … (addr2 :: addr1 :: tmpr :: rah :: ral :: map … (λx.\fst x) to_save))
    304304    (* f_step ≝ *) (translate_step globals)
    305305    (* f_fin ≝ *) (translate_fin_step globals (joint_if_result … def) ral rah to_save)
     
    313313  try #a try #b try #c try #d try #e try #f destruct
    314314  cases a in b; #a1 #a2 normalize nodelta #EQ destruct
    315 | #r1 #r2 #r3 #r4 #r5 #r6 #r7 #r8 #ral #rah #tmpr #addr1 #addr2
    316 change with (? = ?)
     315| #r1 #r2 #r3 #r4 #r5 #r6 #r7 #r8 #ral #rah #tmpr #addr1 #addr2
    317316% (* XXX: FAILS, unintentional list reversal??? *)
    318317]
Note: See TracChangeset for help on using the changeset viewer.