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
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
(UriManager.uri * int * (UriManager.uri * Cic.term) list) list) ->
Cic.term -> unit
-(*
+val injection : Cic.term -> unit
+val discriminate : Cic.term -> unit
val decide_equality : unit -> unit
-val compare : Cic.term -> Cic.term -> unit
-*)
+val compare : Cic.term -> unit
+
(*
val prova_tatticali : unit -> unit