X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.mli;fp=matita%2Fmatita%2FmatitaScript.mli;h=85c4e767a862b95f60627a95f408450c2e249c7d;hb=0fde70bd19b8fdfa72b807b9713a02ad1bd91b5b;hp=e1369617dc91823f70f4646d9856c11335917ce2;hpb=f61ffe97078aab1e47ee1b7f212e707b0412e77e;p=helm.git

diff --git a/matita/matita/matitaScript.mli b/matita/matita/matitaScript.mli
index e1369617d..85c4e767a 100644
--- a/matita/matita/matitaScript.mli
+++ b/matita/matita/matitaScript.mli
@@ -63,12 +63,6 @@ object
 
   (** {2 Current proof} (if any) *)
 
-  (** @return true if there is an ongoing proof, false otherise *)
-  method onGoingProof: unit -> bool
-
-  method proofMetasenv: Cic.metasenv          (** @raise Statement_error *)
-  method proofContext: Cic.context            (** @raise Statement_error *)
-  method proofConclusion: Cic.term            (** @raise Statement_error *)
   method stack: Continuationals.Stack.t       (** @raise Statement_error *)
 
   method setGoal: int option -> unit