X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngine.mli;h=4b7db8fe6346dce46302692bad87de265fa89648;hb=f4c8438e56847bb6e2af5d5cb5858f3ec7dfacb1;hp=c75dc437fe00f5eba77b6b7ec70ef8bb0acc9fda;hpb=be4725575d4dd1d88e13ef388c51f6c9a2f11bc1;p=helm.git

diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index c75dc437f..4b7db8fe6 100644
--- a/helm/gTopLevel/proofEngine.mli
+++ b/helm/gTopLevel/proofEngine.mli
@@ -27,6 +27,10 @@
 val proof : ProofEngineTypes.proof option ref
 val goal : ProofEngineTypes.goal option ref
 
+  (** return a pair of "xml" (as defined in Xml module) representing the current
+  proof type and body, respectively *)
+val get_current_status_as_xml : unit -> Xml.token Stream.t * Xml.token Stream.t
+
   (* start a new goal undoing part of the proof *)
 val perforate : Cic.context -> Cic.term -> Cic.term -> unit
 
@@ -44,7 +48,6 @@ val reduce_in_scratch : Cic.term list -> Cic.term -> Cic.term
 val simpl_in_scratch : Cic.term list -> Cic.term -> Cic.term
 
   (* "primitive" tactics *)
-val can_apply : Cic.term -> bool
 val apply : Cic.term -> unit
 val intros :
  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> unit -> unit