diff options
Diffstat (limited to 'src/hls/RTLParFUgen.v')
| -rw-r--r-- | src/hls/RTLParFUgen.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/RTLParFUgen.v b/src/hls/RTLParFUgen.v index 49ee6e7..a104056 100644 --- a/src/hls/RTLParFUgen.v +++ b/src/hls/RTLParFUgen.v @@ -134,7 +134,7 @@ Definition insert_extra (pt: PTree.t (list instr)) (curr: list (list instr)) | None => ((cycle + 1)%positive, curr :: bb) end. -Definition transl_bb (res: resources) (bb: RTLPar.bb): Errors.res RTLParFU.bblock_body := +Definition transl_bb (res: resources) (bb: list RTLPar.bb): Errors.res RTLParFU.bblock_body := do (litr, n) <- fold_right (transl_seq_block res) (OK (nil, PTree.empty _, 1%positive)) bb; let (li, tr) := litr in OK (snd (fold_right (insert_extra tr) (1%positive, nil) li)). |