diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-02-22 18:42:11 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-22 18:42:11 +0000 |
| commit | 2243443c407a1e951265a9252bac3d3b9b830cbb (patch) | |
| tree | 80ad4560456aa30abc2c1a01b09a86c4ece7b6e9 /src/hls/HTLPargen.v | |
| parent | 1a7f581dc4b67cbfe17936697aec8f85786c844d (diff) | |
| download | vericert-2243443c407a1e951265a9252bac3d3b9b830cbb.tar.gz vericert-2243443c407a1e951265a9252bac3d3b9b830cbb.zip | |
Fix arguments to RBassign and piped
Diffstat (limited to 'src/hls/HTLPargen.v')
| -rw-r--r-- | src/hls/HTLPargen.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index a5b5f41..e1c7ec8 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -691,7 +691,7 @@ Definition translate_inst a (fin rtrn stack preg : reg) (n : node) (i : instr) do cond <- translate_condition c args; ret (a (pred_expr preg (Pvar p)) cond) | RBpiped p f args => error (Errors.msg "HTLPargen.translate_inst: piped") - | RBassign p f dst => error (Errors.msg "HTLPargen.translate_inst: assign") + | RBassign p f src dst => error (Errors.msg "HTLPargen.translate_inst: assign") end. Lemma create_new_state_state_incr: |