aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/AssocMap.v
diff options
context:
space:
mode:
authorMichalis Pardalos <m.pardalos@gmail.com>2021-04-20 21:49:21 +0100
committerMichalis Pardalos <m.pardalos@gmail.com>2021-04-20 21:49:21 +0100
commit57ab80ce060cca19629b99e167740a9bf60b364e (patch)
tree67b3bf80f8aa928bffbe0eeac6d3cf38ada96d4a /src/hls/AssocMap.v
parent7a05aa21b3a94842ceaf103a53209d87d7f095d5 (diff)
downloadvericert-57ab80ce060cca19629b99e167740a9bf60b364e.tar.gz
vericert-57ab80ce060cca19629b99e167740a9bf60b364e.zip
Renumber AssocMaps in HTL modules too
Diffstat (limited to 'src/hls/AssocMap.v')
-rw-r--r--src/hls/AssocMap.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v
index 1d1b77f..68a8416 100644
--- a/src/hls/AssocMap.v
+++ b/src/hls/AssocMap.v
@@ -25,6 +25,7 @@ Require Import vericert.hls.ValueInt.
Definition reg := positive.
Module AssocMap := Maps.PTree.
+Module AssocMap_Properties := Maps.PTree_Properties.
Module AssocMapExt.
Import AssocMap.