1 files changed, 2 insertions, 2 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 2be4fcac..2c1dda5b 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -94,7 +94,7 @@ Coercion BF: final >-> Funclass.
 
 Record iblock_info := { 
   entry: iblock;
-  input_regs: Regset.t (* extra liveness information for BTL functional semantics *)
+  input_regs: Regset.t; (* extra liveness information for BTL functional semantics *)
   binfo: block_info (* Ghost field used in oracles *)
 }.
 
@@ -1285,4 +1285,4 @@ Definition is_goto (ib: iblock): bool :=
   match ib with
   | BF (Bgoto _) _ => true
   | _ => false
-  end.
-\ No newline at end of file
+  end.