Module ProverWhy3

module ProverWhy3: sig .. end
None if the po is trivial

TODO add them only when needed


type goal = {
   file : string;
   theory : string;
   goal : string;
}
val assemble_goal : Wpo.t -> (string list * goal) option
None if the po is trivial
val prove : ?timeout:int -> prover:string -> Wpo.t -> VCS.result Task.task
The string must be a valid why3 prover identifier Return NoResult if it is already proved by Qed
type dp = {
   dp_name : string;
   dp_version : string;
   dp_prover : string;
}
val prover : dp -> VCS.prover
val detect_why3 : (dp list option -> unit) -> unit
val detect_provers : (dp list -> unit) -> unit
val find : string -> dp list -> dp
val parse : string -> dp
module Goal: sig .. end