- (** @return true if there is an ongoing proof, false otherise *)
- method onGoingProof: unit -> bool
-
- method proofMetasenv: Cic.metasenv (** @raise Statement_error *)
- method proofContext: Cic.context (** @raise Statement_error *)
- method proofConclusion: Cic.term (** @raise Statement_error *)