From 24afca4d2800afbcdd80ddf49faaa0b2751c1a77 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 22 Jan 2021 14:48:26 +0000
Subject: Add semantics for RTLBlock

---
 src/hls/RTLBlockInstr.v | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

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

diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index f9d1073..a3f058a 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -47,7 +47,7 @@ Inductive cf_instr : Type :=
 
 Record bblock (bblock_body : Type) : Type := mk_bblock {
     bb_body: bblock_body;
-    bb_exit: option cf_instr
+    bb_exit: cf_instr
   }.
 Arguments mk_bblock [bblock_body].
 Arguments bb_body [bblock_body].
@@ -102,10 +102,6 @@ Inductive instr_state : Type :=
            (m: mem),
     instr_state.
 
-Inductive cf_instr_state : Type :=
-| CfInstrState:
-    forall ()
-
 Section RELSEM.
 
   Context (fundef: Type).
@@ -149,6 +145,4 @@ Section RELSEM.
         forall state,
         step_instr_list state nil state.
 
-  Inductive step_cf_instr:
-
 End RELSEM.
-- 
cgit