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/RTLBlockgen.v | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

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

diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v
index 6b3e9c3..889e104 100644
--- a/src/hls/RTLBlockgen.v
+++ b/src/hls/RTLBlockgen.v
@@ -16,13 +16,11 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From compcert Require
-     RTL.
-From compcert Require Import
-     AST
-     Maps.
-From vericert Require Import
-     RTLBlock.
+Require compcert.backend.RTL.
+Require Import compcert.common.AST.
+Require Import compcert.lib.Maps.
+
+Require Import vericert.hls.RTLBlock.
 
 Parameter partition : RTL.function -> Errors.res function.
 
-- 
cgit