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_proof : Wpo.GOAL.t -> Lang.F.pred
val compute_descr : Wpo.GOAL.t -> Conditions.sequent
val get_descr : Wpo.GOAL.t -> Conditions.sequent
val compute : Wpo.GOAL.t -> unit
val qed_time : Wpo.GOAL.t -> float
end