From ef0d007a20bfe6ed26add13e7459d17ed2bd3eb3 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 4 Nov 2020 11:47:42 +0000
Subject: Quick compile fix

---
 src/hls/RTLBlock.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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

diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
index e5ce9a7..117d21b 100644
--- a/src/hls/RTLBlock.v
+++ b/src/hls/RTLBlock.v
@@ -76,7 +76,7 @@ Definition successors_instr (i : control_flow_inst) : list node :=
   | RBgoto n => n :: nil
   end.
 
-Definition genv := Genv.t fundef unit.
+(* Definition genv := Genv.t fundef unit.
 Definition regset := Regmap.t val.
 
 Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
@@ -165,3 +165,6 @@ Inductive step : state -> trace -> state -> Prop :=
       step (State s f sp pc rs m (mk_bblock nil (RBcond cond args ifso ifnot)) C)
         E0 (State s f sp pc' rs m (mk_bblock nil (RBcond cond args ifso ifnot)) N)
 .
+
+End RELSEM.
+*)
-- 
cgit