- method proof: ProofEngineTypes.proof
- method setProof: ProofEngineTypes.proof -> unit
-
- method goal: ProofEngineTypes.goal option
- method setGoal: ProofEngineTypes.goal option -> unit
-
- (** @raise MatitaTypes.No_proof *)
- method status: ProofEngineTypes.status (* proof, goal *)
- method setStatus: ProofEngineTypes.status -> unit
-
- (** {3 actions} *)
-
- (** return a pair of "xml" (as defined in Xml module) representing the *
- * current proof type and body, respectively *)
- method to_xml: Xml.token Stream.t * Xml.token Stream.t
- end
-
-class proof: uri:UriManager.uri -> typ:Cic.term ->
- object
- (** {3 status} *)
- method status: proofStatus
- method setStatus: proofStatus -> unit
- end