diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-28 12:38:05 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-28 12:38:05 +0200 |
| commit | 8752cea89f862d92d49183fe10d1918588143ab1 (patch) | |
| tree | 2e947a22395702b741c8fac14c7d89ac419c4b5b /scheduling/BTL.v | |
| parent | ef5775ea869701eb04c873174c362b314166bf06 (diff) | |
| download | compcert-kvx-8752cea89f862d92d49183fe10d1918588143ab1.tar.gz compcert-kvx-8752cea89f862d92d49183fe10d1918588143ab1.zip | |
fix some merge errors
Diffstat (limited to 'scheduling/BTL.v')
| -rw-r--r-- | scheduling/BTL.v | 4 |
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. |