sig
type goal = { file : string; theory : string; goal : string; }
val assemble_goal : Wpo.t -> (string list * ProverWhy3.goal) option
val prove : ?timeout:int -> prover:string -> Wpo.t -> VCS.result Task.task
type dp = { dp_name : string; dp_version : string; dp_prover : string; }
val prover : ProverWhy3.dp -> VCS.prover
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