aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/IfConversion.v
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2022-05-25 18:26:20 +0100
committerYann Herklotz <git@yannherklotz.com>2022-05-25 18:26:20 +0100
commit81618c8d08bd70effcbe3ec087f69106e3cedf95 (patch)
tree5265bc6bf311c5e744cc52640327cdfb06dad2f2 /src/hls/IfConversion.v
parentb3e2078df318a2d5e54de0b09963f37d63327f0a (diff)
downloadvericert-81618c8d08bd70effcbe3ec087f69106e3cedf95.tar.gz
vericert-81618c8d08bd70effcbe3ec087f69106e3cedf95.zip
Translate the base languages
Diffstat (limited to 'src/hls/IfConversion.v')
-rw-r--r--src/hls/IfConversion.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 2516109..4e62a68 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -106,7 +106,7 @@ Fixpoint get_loops (b: bourdoncle): list node :=
end.
Definition is_loop (b: list node) (n: node) :=
- any (fun x => Pos.eqb x n) b.
+ any (Pos.eqb n) b.
Definition is_flat_cfi (n: cf_instr) :=
match n with