diff options
-rw-r--r-- | scheduling/BTL_SEimpl.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index 65d16d01..36f49d28 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -1096,13 +1096,12 @@ Lemma hrexec_rec_correct1 ctx ib: WHEN hrexec_rec (cf ctx) ib hrs rk ~> rst THEN rst_refines ctx rst st. Proof. - induction ib; try (wlp_simplify; fail). + induction ib; try (wlp_simplify; try (eapply CONT; eauto); fail). - (* BF *) wlp_simplify; exploit tr_hrs_correct; eauto. intros; constructor; auto. intros X; apply H0 in X. exploit hrexec_final_sfv_correct; eauto. - - (* Bnop *) wlp_simplify; eapply CONT; eauto. - (* Bseq *) wlp_simplify. eapply IHib1. 3-7: eauto. |