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 ++++-
 src/hls/RTLPar.v   | 3 ++-
 2 files changed, 6 insertions(+), 2 deletions(-)

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.
+*)
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
index 038ae32..0e94fd5 100644
--- a/src/hls/RTLPar.v
+++ b/src/hls/RTLPar.v
@@ -76,7 +76,7 @@ Definition successors_instr (i : control_flow_inst) : list node :=
   | RPgoto n => n :: nil
   end.
 
-Inductive state : Type :=
+(*Inductive state : Type :=
   | State:
       forall (stack: list stackframe) (**r call stack *)
              (f: function)            (**r current function *)
@@ -96,3 +96,4 @@ Inductive state : Type :=
              (v: val)                 (**r return value for the call *)
              (m: mem),                (**r memory state *)
       state.
+*)
-- 
cgit