diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-09-02 09:16:31 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-09-02 09:16:31 +0200 |
| commit | 3eb8d3f6f154c7e87f634fcae224fe9fa39d52c6 (patch) | |
| tree | 4952010e868f7aa42dca046108e2f67b9edfa5c9 /scheduling | |
| parent | d0819d14a514c81cd9437de467d4880965bc3a7f (diff) | |
| download | compcert-kvx-3eb8d3f6f154c7e87f634fcae224fe9fa39d52c6.tar.gz compcert-kvx-3eb8d3f6f154c7e87f634fcae224fe9fa39d52c6.zip | |
fix compil for coq 8.13.2
Diffstat (limited to 'scheduling')
| -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. |