From 0821c3a96b3a0c903d722dc8c64bc044e8b2563b Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 22 Sep 2021 09:07:59 +0200 Subject: fix Compiler.vexpand --- driver/Compiler.vexpand | 19 ------------------- 1 file changed, 19 deletions(-) diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 9ff9ac6b..4d465839 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -316,27 +316,8 @@ EXPAND_RTL_FORWARD_SIMULATIONS eapply compose_forward_simulations. eapply match_if_simulation. eassumption. eapply Deadcodeproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply RTLpathLivegenproof.transf_program_correct; eassumption. - pose proof RTLpathLivegenproof.all_fundef_liveness_ok as X'. - refine (modusponens _ _ (X' _ _ _) _); eauto. intro. - - eapply compose_forward_simulations. - eapply MyRTLpathSchedulerproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply RTLpathproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply Liftifproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply Renumberproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. eapply CSE3proof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. eapply Deadcodeproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. eapply RTLTunnelingproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. eapply RTLpathLivegenproof.transf_program_correct; eassumption. pose proof RTLpathLivegenproof.all_fundef_liveness_ok as X'. -- cgit