From 929ca73f8aed8c122b93527c545a38dd82d52647 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 22 Jan 2021 17:41:37 +0000
Subject: Fix imports to remove warnings when compiling

---
 src/hls/AssocMap.v | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'src/hls/AssocMap.v')

diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v
index 51afed7..1d1b77f 100644
--- a/src/hls/AssocMap.v
+++ b/src/hls/AssocMap.v
@@ -17,8 +17,10 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From vericert Require Import Vericertlib ValueInt.
-From compcert Require Import Maps.
+Require Import compcert.lib.Maps.
+
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.ValueInt.
 
 Definition reg := positive.
 
-- 
cgit