sig
val simplify :
?start:(Wp.Wpo.t -> unit) ->
?result:(Wp.Wpo.t -> Wp.VCS.prover -> Wp.VCS.result -> unit) ->
Wp.Wpo.t -> bool Task.task
val prove :
Wp.Wpo.t ->
?config:Wp.VCS.config ->
?mode:Wp.VCS.mode ->
?start:(Wp.Wpo.t -> unit) ->
?progress:(Wp.Wpo.t -> string -> unit) ->
?result:(Wp.Wpo.t -> Wp.VCS.prover -> Wp.VCS.result -> unit) ->
Wp.VCS.prover -> bool Task.task
val spawn :
Wp.Wpo.t ->
delayed:bool ->
?config:Wp.VCS.config ->
?start:(Wp.Wpo.t -> unit) ->
?progress:(Wp.Wpo.t -> string -> unit) ->
?result:(Wp.Wpo.t -> Wp.VCS.prover -> Wp.VCS.result -> unit) ->
?success:(Wp.Wpo.t -> Wp.VCS.prover option -> unit) ->
?pool:Task.pool -> (Wp.VCS.mode * Wp.VCS.prover) list -> unit
end