X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaProof.mli;h=97551eb8ce719c749ada69943f96c8566ecea570;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=e74efdf7df47f171eabf34b3749268c6a8ba8071;hpb=b5d69130dd83587b5fb9cbb39251aaa8df8c456e;p=helm.git

diff --git a/helm/matita/matitaProof.mli b/helm/matita/matitaProof.mli
index e74efdf7d..97551eb8c 100644
--- a/helm/matita/matitaProof.mli
+++ b/helm/matita/matitaProof.mli
@@ -23,52 +23,33 @@
  * 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} *)
 
-(* TODO these are just some examples, a lot of other tactics/tacticals must be
- * added here *)
+(* 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
+                  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