* http://helm.cs.unibo.it/
*)
-class proofStatus: uri:UriManager.uri -> typ:Cic.term ->
- object
- inherit MatitaTypes.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 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
-
-(** {2 tactic commands builders} *)
-
-(* TODO Zack: these are just some examples, a lot of other tactics/tacticals
- * must be added here *)
-
-val intros: ?namer:MatitaTypes.namer ->
- proofStatus -> MatitaTypes.command
-
-val reflexivity: proofStatus -> MatitaTypes.command
-val symmetry: proofStatus -> MatitaTypes.command
-val transitivity: Cic.term -> proofStatus -> MatitaTypes.command
-
-val exists: proofStatus -> MatitaTypes.command
-val split: proofStatus -> MatitaTypes.command
-val left: proofStatus -> MatitaTypes.command
-val right: proofStatus -> MatitaTypes.command
-
-val assumption: proofStatus -> MatitaTypes.command
+ (** create a new proof object. Typecheck the resulting sequent.
+ * @param typ goal type
+ * @param metasenv metasenv returned by the disambiguator, this will not be
+ * the final metasenv of the first sequence, meta corresponding to typ will
+ * be added
+ * @param uri new proof uri *)
+val proof:
+ ?uri:UriManager.uri ->
+ metasenv:Cic.metasenv -> typ:Cic.term ->
+ unit ->
+ MatitaTypes.proof