aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/HTLgen.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/hls/HTLgen.v')
-rw-r--r--src/hls/HTLgen.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index 3f4e513..b879c8d 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -32,6 +32,7 @@ Require Import vericert.hls.AssocMap.
Require Import vericert.hls.HTL.
Require Import vericert.hls.ValueInt.
Require Import vericert.hls.Verilog.
+Require Import vericert.hls.FunctionalUnits.
#[local] Hint Resolve AssocMap.gempty : htlh.
#[local] Hint Resolve AssocMap.gso : htlh.