Skip to content
Snippets Groups Projects
Commit e04471a3 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] use Server async call for Qed

parent 2762f209
No related branches found
No related tags found
No related merge requests found
...@@ -76,7 +76,7 @@ let run_prover wpo ?config ?(mode=Batch) ?progress ?result prover = ...@@ -76,7 +76,7 @@ let run_prover wpo ?config ?(mode=Batch) ?progress ?result prover =
Task.return (VCS.is_valid res) Task.return (VCS.is_valid res)
let simplify ?start ?result wpo = let simplify ?start ?result wpo =
Task.call Server.Main.async
(fun wpo -> (fun wpo ->
let r = Wpo.get_result wpo VCS.Qed in let r = Wpo.get_result wpo VCS.Qed in
VCS.( r.verdict == Valid ) || VCS.( r.verdict == Valid ) ||
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment