diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-04-23 09:37:02 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-04-23 09:37:02 +0100 |
| commit | 6f9d16bb67f32463d98771f3f155297c4ea4b3b7 (patch) | |
| tree | 1d04c6794b53981a340af2d3b72971d8c9a02d8e /src/hls/RTLParFUgen.v | |
| parent | 1dce00e3afe9398a84239cc5f5d44c68b0b5c474 (diff) | |
| download | vericert-6f9d16bb67f32463d98771f3f155297c4ea4b3b7.tar.gz vericert-6f9d16bb67f32463d98771f3f155297c4ea4b3b7.zip | |
Fix translation passes with new semantics
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 a104056..49ee6e7 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: list RTLPar.bb): Errors.res RTLParFU.bblock_body := +Definition transl_bb (res: resources) (bb: 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)). |