module GOAL:sig
..end
type
t = {
|
mutable time : |
|
mutable simplified : |
|
mutable sequent : |
|
mutable obligation : |
val empty : Conditions.hypotheses
val dummy : t
val trivial : t
val make : Conditions.sequent -> t
val is_trivial : t -> bool
val apply : (Conditions.sequent -> Conditions.sequent) -> t -> unit
val preprocess : t -> unit
val dkey : Log.category
val compute : t -> unit
val compute_proof : t -> Lang.F.pred
val compute_descr : t -> Conditions.sequent
val get_descr : t -> Conditions.sequent
val qed_time : t -> float