diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-02-05 21:56:12 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-02-05 21:56:12 +0000 |
| commit | 304762a8405d0e8f2edc3d0d9caaf063bddbb0ca (patch) | |
| tree | 59eb9026b86268659298ad228d9478bb17340787 /src/hls/GiblePargen.v | |
| parent | a79914b49d81e6be31dd936b4c70a5a01ab498e2 (diff) | |
| download | vericert-304762a8405d0e8f2edc3d0d9caaf063bddbb0ca.tar.gz vericert-304762a8405d0e8f2edc3d0d9caaf063bddbb0ca.zip | |
Switch to half lazy evaluation
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; |