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