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