snapshot

[helm.git] / helm / matita / matitaProof.mli

diff --git a/helm/matita/matitaProof.mli b/helm/matita/matitaProof.mli
index 97551eb8ce719c749ada69943f96c8566ecea570..9293e330afa1c6586fd9d70f90d8be58c2044324 100644 (file)
--- a/helm/matita/matitaProof.mli
+++ b/helm/matita/matitaProof.mli
@@ -23,33 +23,15 @@
  * http://helm.cs.unibo.it/
  *)
 
-val proofStatus:
-  typ:Cic.term -> ?metasenv:Cic.metasenv -> ?uri:UriManager.uri -> unit ->
-    MatitaTypes.proofStatus
-
-  (** inverse function of proofStatus#toString / proofStatus#toOutchan *)
-val proofStatus_of_string: string -> MatitaTypes.proofStatus
-
+  (** 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:
-  typ:Cic.term -> ?metasenv:Cic.metasenv -> ?uri:UriManager.uri -> unit ->
+  ?uri:UriManager.uri ->
+  metasenv:Cic.metasenv -> typ:Cic.term ->
+  unit ->
     MatitaTypes.proof
 
-(** {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 ->
-                  MatitaTypes.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:       MatitaTypes.proofStatus -> MatitaTypes.command
-val split:        MatitaTypes.proofStatus -> MatitaTypes.command
-val left:         MatitaTypes.proofStatus -> MatitaTypes.command
-val right:        MatitaTypes.proofStatus -> MatitaTypes.command
-
-val assumption:   MatitaTypes.proofStatus -> MatitaTypes.command
-