From f59ff208a301bf3f04aab350d9f0b3b217ddeac3 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Mon, 19 Jul 2021 14:20:53 +0200
Subject: Finish implem proof, need to adapt scheduler proof

---
 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 95363194..91e650e8 100644
--- a/scheduling/BTL_Schedulerproof.v
+++ b/scheduling/BTL_Schedulerproof.v
@@ -105,11 +105,12 @@ Lemma transf_fundef_correct f f':
   transf_fundef f = OK f' -> match_fundef f f'.
 Proof.
   intros TRANSF; destruct f; simpl; inv TRANSF.
+Admitted. (*
   + exploit transf_function_correct; eauto.
     econstructor. intros MATCH_F.
     eapply match_Internal; eauto.
   + eapply match_External.
-Qed.
+             Qed.*)
 
 Lemma function_ptr_preserved:
   forall v f,
-- 
cgit