diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-10-20 19:05:00 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-10-20 19:05:00 +0100 |
| commit | 9db69b471864cb9e3868dd2c82bc0e2df3955b51 (patch) | |
| tree | b56e41f85768244ad1148fc6e541444f0e614835 /src/hls/DHTLgen.v | |
| parent | 26db7d1fe8c93e88ccecc33254d75e4b90844545 (diff) | |
| download | vericert-9db69b471864cb9e3868dd2c82bc0e2df3955b51.tar.gz vericert-9db69b471864cb9e3868dd2c82bc0e2df3955b51.zip | |
Fix more proofs moving to proving instructions
Diffstat (limited to 'src/hls/DHTLgen.v')
| -rw-r--r-- | src/hls/DHTLgen.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/DHTLgen.v b/src/hls/DHTLgen.v index 49d2c87..d573dda 100644 --- a/src/hls/DHTLgen.v +++ b/src/hls/DHTLgen.v @@ -356,7 +356,7 @@ Definition transf_seq_block (ctrl: control_regs) (d: datapath) (ni: node * SubPa let (n, bb) := ni in match d ! n with | None => - do (_pred, stmnt) <- transf_parallel_block ctrl bb; + do (_pred, stmnt) <- transf_chained_block ctrl (Ptrue, Vskip) (concat bb); OK (PTree.set n stmnt d) | _ => Error (msg "DHTLgen: overwriting location") end. |