diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-07-22 17:54:54 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-07-22 17:54:54 +0200 |
| commit | 8de8dc6616c49018c6151887f76ea08c8f1ff04e (patch) | |
| tree | da7fcb77c893c3980feb86e9a2772ed6019981cf /scheduling/BTL_Schedulerproof.v | |
| parent | 6adfc52c130ee73cf6ee2ee8b85ed8b5e5024a4a (diff) | |
| download | compcert-kvx-8de8dc6616c49018c6151887f76ea08c8f1ff04e.tar.gz compcert-kvx-8de8dc6616c49018c6151887f76ea08c8f1ff04e.zip | |
nothing admitted !!
Diffstat (limited to 'scheduling/BTL_Schedulerproof.v')
| -rw-r--r-- | scheduling/BTL_Schedulerproof.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v index 05028f11..27efe56f 100644 --- a/scheduling/BTL_Schedulerproof.v +++ b/scheduling/BTL_Schedulerproof.v @@ -95,7 +95,8 @@ Qed. Lemma transf_function_correct f f': transf_function f = OK f' -> match_function f f'. Proof. - unfold transf_function. intros H. monadInv H. + unfold transf_function. intros H. + assert (OH: transf_function f = OK f') by auto. monadInv H. econstructor; eauto. eapply check_symbolic_simu_input_equiv; eauto. eapply check_symbolic_simu_correct; eauto. |