From 8de8dc6616c49018c6151887f76ea08c8f1ff04e Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 22 Jul 2021 17:54:54 +0200 Subject: nothing admitted !! --- scheduling/BTL_Schedulerproof.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'scheduling/BTL_Schedulerproof.v') 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. -- cgit