sig
  type t
  val dummy : Wpo.GOAL.t
  val trivial : Wpo.GOAL.t
  val is_trivial : Wpo.GOAL.t -> bool
  val make : Conditions.sequent -> Wpo.GOAL.t
  val compute : pid:WpPropId.prop_id -> Wpo.GOAL.t -> unit
  val compute_proof : pid:WpPropId.prop_id -> Wpo.GOAL.t -> Lang.F.pred
  val compute_descr :
    pid:WpPropId.prop_id -> Wpo.GOAL.t -> Conditions.sequent
  val get_descr : Wpo.GOAL.t -> Conditions.sequent
  val qed_time : Wpo.GOAL.t -> float
end