+ (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
+ end
+
+class type proofStatus =
+ object
+ inherit subject
+
+ (** {3 properties} *)
+
+ 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 toXml: Xml.token Stream.t * Xml.token Stream.t
+ method toString: string
+ end
+
+class type proof =
+ object
+ (** {3 status} *)
+ method status: proofStatus
+ method setStatus: proofStatus -> unit
+ end
+
+ (** interpreter for toplevel phrases given via console *)
+class type interpreter =
+ object
+ method evalPhrase: string -> unit