1 files changed, 1 insertions, 0 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 064297f1..d55a0415 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -819,6 +819,7 @@ Fixpoint expand (ib: iblock) (k: option iblock): iblock :=
   | Bseq ib1 ib2 => expand ib1 (Some (expand ib2 k))
   | Bcond cond args ib1 ib2 i => 
      Bcond cond args (expand ib1 k) (expand ib2 k) i
+  | BF fin => fin
   | ib => 
     match k with 
     | None => ib