From 2243443c407a1e951265a9252bac3d3b9b830cbb Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 22 Feb 2021 18:42:11 +0000 Subject: Fix arguments to RBassign and piped --- src/hls/HTLPargen.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/hls/HTLPargen.v') 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: -- cgit