sig
  type prover
  type result
  type po
  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 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 get_gid : Dynamic_plugins.Wp.Wpo.po -> string
  val get_property : Dynamic_plugins.Wp.Wpo.po -> Property.t
end