diff options
Diffstat (limited to 'src/hls/GiblePargen.v')
| -rw-r--r-- | src/hls/GiblePargen.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index eaf452a..8a2c629 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -215,7 +215,7 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest | RBsetpred p' c args p => let new_pred := (from_pred_op f.(forest_preds) (dfltp p' ∧ pred) - → from_predicated true f.(forest_preds) (seq_app (pred_ret (PEsetpred c)) + → from_predicated true f.(forest_preds) (seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f)))) in do _ <- is_initial_pred f p; |