* http://helm.cs.unibo.it/
*)
-class proofStatus: uri:UriManager.uri -> typ:Cic.term ->
- object
- inherit MatitaTypes.subject
+val proofStatus:
+ typ:Cic.term -> ?metasenv:Cic.metasenv -> ?uri:UriManager.uri -> unit ->
+ MatitaTypes.proofStatus
- (** {3 properties} *)
+ (** inverse function of proofStatus#toString / proofStatus#toOutchan *)
+val proofStatus_of_string: string -> MatitaTypes.proofStatus
- 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
+val proof:
+ typ:Cic.term -> ?metasenv:Cic.metasenv -> ?uri:UriManager.uri -> unit ->
+ MatitaTypes.proof
(** {2 tactic commands builders} *)
* must be added here *)
val intros: ?namer:MatitaTypes.namer ->
- proofStatus -> MatitaTypes.command
+ MatitaTypes.proofStatus -> MatitaTypes.command
-val reflexivity: proofStatus -> MatitaTypes.command
-val symmetry: proofStatus -> MatitaTypes.command
-val transitivity: Cic.term -> proofStatus -> MatitaTypes.command
+val reflexivity: MatitaTypes.proofStatus -> MatitaTypes.command
+val symmetry: MatitaTypes.proofStatus -> MatitaTypes.command
+val transitivity: Cic.term -> MatitaTypes.proofStatus -> MatitaTypes.command
-val exists: proofStatus -> MatitaTypes.command
-val split: proofStatus -> MatitaTypes.command
-val left: proofStatus -> MatitaTypes.command
-val right: proofStatus -> MatitaTypes.command
+val exists: MatitaTypes.proofStatus -> MatitaTypes.command
+val split: MatitaTypes.proofStatus -> MatitaTypes.command
+val left: MatitaTypes.proofStatus -> MatitaTypes.command
+val right: MatitaTypes.proofStatus -> MatitaTypes.command
-val assumption: proofStatus -> MatitaTypes.command
+val assumption: MatitaTypes.proofStatus -> MatitaTypes.command