val goal : ProofEngineTypes.goal option ref
(** return a pair of "xml" (as defined in Xml module) representing the current
val goal : ProofEngineTypes.goal option ref
(** return a pair of "xml" (as defined in Xml module) representing the current
val discriminate : Cic.term -> unit
val decide_equality : unit -> unit
val compare : Cic.term -> unit
val discriminate : Cic.term -> unit
val decide_equality : unit -> unit
val compare : Cic.term -> unit