sig
type goal_id = { gfile : string; gtheory : string; ggoal : string; }
val assemble_wpo : Wpo.t -> (string list * ProverWhy3.goal_id) option
val prove : Wpo.t -> prover:string -> VCS.result Task.task
val call_ide :
includes:string list ->
files:string list -> session:string -> bool 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
end