1 files changed, 0 insertions, 18 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index d55a0415..10a000a8 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -833,21 +833,3 @@ Lemma expand_correct ib: forall k,
 Proof.
   induction ib; simpl; intros; try autodestruct; auto.
 Qed.
-
-Lemma expand_None_correct ib: 
-   is_expand (expand ib None).
-Proof.
-  apply expand_correct; simpl; auto.
-Qed.
-
-Definition expand_code (cfg: code): code :=
-  (PTree.map (fun _ ib => {| entry:=expand ib.(entry) None; input_regs := ib.(input_regs) |}) cfg).
-
-Lemma expand_code_correct cfg pc ib :
-  (expand_code cfg)!pc=Some ib -> is_expand (ib.(entry)).
-Proof.
-  unfold expand_code.
-  rewrite PTree.gmap.
-  destruct (cfg!pc); simpl; intros; try_simplify_someHyps.
-  apply expand_None_correct; auto.
-Qed.