diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-09 22:41:40 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-09 22:41:40 +0200 |
| commit | c78393a5d4d13d0f2cd7f0a73756d6bb598b5ae4 (patch) | |
| tree | 34d4e1560a663080217fb251e0fc92d632dc950d /scheduling/RTLtoBTLproof.v | |
| parent | 08b39b2025951a9655939c1377f6e53b346c6821 (diff) | |
| download | compcert-kvx-c78393a5d4d13d0f2cd7f0a73756d6bb598b5ae4.tar.gz compcert-kvx-c78393a5d4d13d0f2cd7f0a73756d6bb598b5ae4.zip | |
mib_exit draft
Diffstat (limited to 'scheduling/RTLtoBTLproof.v')
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 023837f9..1db088d2 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -264,12 +264,13 @@ Proof. - (* mib_BF *) admit. - (* mib_exit *) - (* destruct t. - 2: { + (* + simpl in *. + eapply iblock_istep_run_equiv in BTL_RUN. + inv BTL_RUN. eexists; left. eexists; split. + eapply exec_iblock; eauto. econstructor; repeat eexists. - eapply iblock_istep_run_equiv; eauto. inv STEP. eapply exec_Bgoto.*) admit. - (* mib_seq *) |