sig   type goal = { file : string; theory : string; goal : string; }   val assemble_wpo : Wpo.t -> (string list * ProverWhy3.goal) option   val prove : Wpo.t -> prover:string -> VCS.result Task.task   type dp = { dp_name : string; dp_version : string; dp_prover : string; }   val detect_why3 : (ProverWhy3.dp list option -> unit) -> unit   val detect_provers : (ProverWhy3.dp list -> unit) -> unit   val find : string -> ProverWhy3.dp list -> ProverWhy3.dp   val parse : string -> ProverWhy3.dp   module Goal :     sig       type t = ProverWhy3.goal       val compare : ProverWhy3.Goal.t -> ProverWhy3.Goal.t -> int       val pretty : Format.formatter -> ProverWhy3.Goal.t -> unit     end end