From 3eb8d3f6f154c7e87f634fcae224fe9fa39d52c6 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Thu, 2 Sep 2021 09:16:31 +0200
Subject: fix compil for coq 8.13.2

---
 scheduling/BTL_SEimpl.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'scheduling')

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.
-- 
cgit