simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-09 12:45:48 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(proof): add neg-normalization

Browse source
This commit is contained in:
Simon Cruanes 2021-11-14 22:50:05 -05:00
parent ffa450ba08
commit 7d70994758
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/base/Proof_quip.ml
View file

@ -237,7 +237,7 @@ end = struct
Array.iter add_needed_step exprs; Array.iter add_needed_step exprs;
let p = lazy ( let p = lazy (
let exprs = Util.array_to_list_map L_terms.find exprs in let exprs = Util.array_to_list_map L_terms.find exprs in
P.bool_c rule exprs P.nn @@ P.bool_c rule exprs
) in ) in
L_proofs.add lid p; L_proofs.add lid p;