diff options
-rw-r--r-- | scheduling/BTLtoRTLproof.v | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 67a01c20..3944e756 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -4,10 +4,6 @@ Require Import RTL Op Registers OptionMonad BTL. Require Import Errors Linking BTLtoRTL. - -(**********************************) -(* TODO Put this in an other file *) - Require Import Linking. Lemma transf_function_correct f f': @@ -175,7 +171,6 @@ Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin match ofin with | None => exists pc1,(opc = Some pc1) /\ plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1) | Some fin => - (* XXX A CHANGER ? *) exists isfst' pc1, match_iblock dupmap (RTL.fn_code f') isfst' pc1 fin None /\ cond_star_step (isfst = isfst') (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1) end. @@ -218,7 +213,7 @@ Proof. eapply plus_trans; eauto. - (* exec_cond *) inv MIB. - assert (JOIN: is_join_opt opc1 opc2 opc). { exact H10. } clear H10. + rename H10 into JOIN. (* is_join_opt opc1 opc2 opc *) destruct b; exploit IHIBIS; eauto. + (* taking ifso *) destruct ofin; simpl. |