From 99e735af1f7726da2903409758bee202cf47c6a4 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Mon, 17 May 2021 16:02:57 +0200
Subject: Lemmas on ISTEP

---
 scheduling/BTL.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'scheduling/BTL.v')

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
-- 
cgit