diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-05 08:51:51 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-05 08:51:51 +0200 |
| commit | f427f9b257baee8a962a4b3e6c1e3c1804fd65da (patch) | |
| tree | dea0b001bcb0ad875b6a675dae35f4639869f79c /scheduling/BTLtoRTLproof.v | |
| parent | bf2ed66aa8c87b95c1d57cdd7f22dc131c7728cf (diff) | |
| download | compcert-kvx-f427f9b257baee8a962a4b3e6c1e3c1804fd65da.tar.gz compcert-kvx-f427f9b257baee8a962a4b3e6c1e3c1804fd65da.zip | |
clean deprecated comments
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
| -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. |