From 8752cea89f862d92d49183fe10d1918588143ab1 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 28 May 2021 12:38:05 +0200 Subject: fix some merge errors --- scheduling/BTL.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'scheduling/BTL.v') 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. -- cgit