- added and exposed get_current_status_as_xml

[helm.git] / helm / gTopLevel / proofEngine.mli

diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index c75dc437fe00f5eba77b6b7ec70ef8bb0acc9fda..4b7db8fe6346dce46302692bad87de265fa89648 100644 (file)
--- 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