sig
type result
type prover
type po
val iter_on_goals : (Dynamic_plugins.Wp.Wpo.po -> unit) -> unit
val is_valid : Dynamic_plugins.Wp.Wpo.result -> bool
val goals_of_property : Property.t -> Dynamic_plugins.Wp.Wpo.po list
val get_result :
Dynamic_plugins.Wp.Wpo.po ->
Dynamic_plugins.Wp.Wpo.prover -> Dynamic_plugins.Wp.Wpo.result
val file_for_log_proof :
Dynamic_plugins.Wp.Wpo.po ->
Dynamic_plugins.Wp.Wpo.prover -> string * string
val prover_of_name : string -> Dynamic_plugins.Wp.Wpo.prover option
val get_gid : Dynamic_plugins.Wp.Wpo.po -> string
val get_property : Dynamic_plugins.Wp.Wpo.po -> Property.t
end