aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/RTLPar.v
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-01-22 17:20:34 +0000
committerYann Herklotz <git@yannherklotz.com>2021-01-22 17:20:34 +0000
commit2f313b9ced2e74702e4881f858cbebb205b2cdd5 (patch)
tree10c24175e537847086bd33e255daf9c8bc800698 /src/hls/RTLPar.v
parent8f6bc3b0b036c9ede3bb9bb69763316449b05be4 (diff)
downloadvericert-2f313b9ced2e74702e4881f858cbebb205b2cdd5.tar.gz
vericert-2f313b9ced2e74702e4881f858cbebb205b2cdd5.zip
Fix types with new changes in RTLBlock
Also formatted some files so that they are under 80 columns, which is much nicer to read.
Diffstat (limited to 'src/hls/RTLPar.v')
-rw-r--r--src/hls/RTLPar.v3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
index af6b0ab..94a1a20 100644
--- a/src/hls/RTLPar.v
+++ b/src/hls/RTLPar.v
@@ -30,7 +30,8 @@ Require Import compcert.verilog.Op.
Require Import vericert.hls.RTLBlockInstr.
-Definition bblock := RTLBlockInstr.bblock (list (list instr)).
+Definition bblock_body := list (list instr).
+Definition bblock := RTLBlockInstr.bblock bblock_body.
Definition code : Type := PTree.t bblock.