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