diff options
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. |