aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/GiblePargen.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/hls/GiblePargen.v')
-rw-r--r--src/hls/GiblePargen.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v
index dae1efc..b7f4446 100644
--- a/src/hls/GiblePargen.v
+++ b/src/hls/GiblePargen.v
@@ -184,7 +184,7 @@ Fixpoint apredicated_to_apred_op (b: bool) (a: apredicated expression): apred_op
match a with
| NE.singleton (p, e) => Pimplies p (Plit (b, e))
| (p, e) ::| r =>
- Pand (Pimplies p (Plit (true, e))) (apredicated_to_apred_op b r)
+ Pand (Pimplies p (Plit (b, e))) (apredicated_to_apred_op b r)
end.
(* Fixpoint get_pred' (f: forest) (ap: pred_op): option apred_op := *)