aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/GiblePargen.v
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2022-07-31 22:33:50 +0100
committerYann Herklotz <git@yannherklotz.com>2022-07-31 22:33:50 +0100
commit2321c5e73833e7cac019d6a4198489e37129c15e (patch)
tree00bf235cbadf40ee67e467ed06b4905cbb7d980b /src/hls/GiblePargen.v
parent8db521d92806325dff87084aa08a9f3b152da1e2 (diff)
downloadvericert-2321c5e73833e7cac019d6a4198489e37129c15e.tar.gz
vericert-2321c5e73833e7cac019d6a4198489e37129c15e.zip
Add current changes
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 := *)