diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-09-22 09:07:59 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-09-22 09:07:59 +0200 |
| commit | 0821c3a96b3a0c903d722dc8c64bc044e8b2563b (patch) | |
| tree | 22250a4ac501197233eb8962a8a6c0f712f5f6a2 | |
| parent | d8fbc3e401040cc3438545b00923ce8cfda5bdd5 (diff) | |
| download | compcert-kvx-0821c3a96b3a0c903d722dc8c64bc044e8b2563b.tar.gz compcert-kvx-0821c3a96b3a0c903d722dc8c64bc044e8b2563b.zip | |
fix Compiler.vexpand
| -rw-r--r-- | driver/Compiler.vexpand | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 9ff9ac6b..4d465839 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -317,26 +317,7 @@ EXPAND_RTL_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'. |