module ProverCoq: sig .. end
sig
end
val prove : VCS.mode -> Wpo.t -> VCS.result Task.task
VCS.mode -> Wpo.t -> VCS.result Task.task