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