diff options
Diffstat (limited to 'src/hls/RTLBlockInstr.v')
| -rw-r--r-- | src/hls/RTLBlockInstr.v | 8 |
1 files changed, 1 insertions, 7 deletions
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. |