From 9ce1b23f6361d8070490df1269a7bc53aa215efb Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Wed, 21 Jul 2021 12:16:27 +0200
Subject: expansions btl proofs

---
 scheduling/BTL_Schedulerproof.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'scheduling/BTL_Schedulerproof.v')

diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v
index 9b0383ae..05028f11 100644
--- a/scheduling/BTL_Schedulerproof.v
+++ b/scheduling/BTL_Schedulerproof.v
@@ -98,19 +98,17 @@ Proof.
   unfold transf_function. intros H. monadInv H.
   econstructor; eauto.
   eapply check_symbolic_simu_input_equiv; eauto.
-Admitted. (*
   eapply check_symbolic_simu_correct; eauto.
-             Qed.*)
+Qed.
 
 Lemma transf_fundef_correct f f':
   transf_fundef f = OK f' -> match_fundef f f'.
 Proof.
   intros TRANSF; destruct f; simpl; inv TRANSF.
-Admitted. (*
   + monadInv H0. exploit transf_function_correct; eauto.
     constructor; auto.
   + eapply match_External.
-             Qed.*)
+Qed.
 
 Lemma function_ptr_preserved:
   forall v f,
-- 
cgit