diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-07-31 22:33:50 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-07-31 22:33:50 +0100 |
commit | 2321c5e73833e7cac019d6a4198489e37129c15e (patch) | |
tree | 00bf235cbadf40ee67e467ed06b4905cbb7d980b /src/hls/GiblePargen.v | |
parent | 8db521d92806325dff87084aa08a9f3b152da1e2 (diff) | |
download | vericert-2321c5e73833e7cac019d6a4198489e37129c15e.tar.gz vericert-2321c5e73833e7cac019d6a4198489e37129c15e.zip |
Add current changes
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 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 := *) |