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

proof: normalize clauses in rw

Browse source
This commit is contained in:
Simon Cruanes 2021-11-10 18:30:12 -05:00
parent a8a851a7de
commit ffa450ba08
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

@ -215,7 +215,7 @@ end = struct
let name = name_clause lid in let name = name_clause lid in
let step = lazy ( let step = lazy (
let c = L_proofs.find c in let c = P.nn @@ L_proofs.find c in
let using = Util.array_to_list_map L_proofs.find using in let using = Util.array_to_list_map L_proofs.find using in
let res = !! res in let res = !! res in
P.S_step_c {name; res; proof=P.Clause_rw {res; c0=c; using}} P.S_step_c {name; res; proof=P.Clause_rw {res; c0=c; using}}