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
(* reduction tactics *)
-val whd : Cic.term -> unit
-val reduce : Cic.term -> unit
-val simpl : Cic.term -> unit
+val whd : Cic.term list -> unit
+val reduce : Cic.term list -> unit
+val simpl : Cic.term list -> unit
val fold_whd : Cic.term -> unit
val fold_reduce : Cic.term -> unit
val fold_simpl : Cic.term -> unit
(* scratch area reduction tactics *)
-val whd_in_scratch : Cic.term -> Cic.term -> Cic.term
-val reduce_in_scratch : Cic.term -> Cic.term -> Cic.term
-val simpl_in_scratch : Cic.term -> Cic.term -> Cic.term
+val whd_in_scratch : Cic.term list -> Cic.term -> Cic.term
+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 : unit -> unit
-val cut : Cic.term -> unit
-val letin : Cic.term -> unit
+val intros :
+ ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> unit -> unit
+val cut :
+ ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term -> unit
+val letin :
+ ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term -> unit
val exact : Cic.term -> unit
val elim_intros_simpl : Cic.term -> unit
val change : goal_input:Cic.term -> input:Cic.term -> unit
val assumption : unit -> unit
-val generalize : Cic.term -> unit
+val generalize :
+ ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+ Cic.term list -> unit
val absurd : Cic.term -> unit
val contradiction : 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