*)
(* proof engine status *)
-val proof : ProofEngineTypes.proof option ref
+val get_proof : unit -> ProofEngineTypes.proof option
+val set_proof : ProofEngineTypes.proof option -> unit
val goal : ProofEngineTypes.goal option ref
(** return a pair of "xml" (as defined in Xml module) representing the current
val rewrite_simpl : Cic.term -> unit
val rewrite_back_simpl : Cic.term -> unit
val replace : goal_input:Cic.term -> input:Cic.term -> unit
+val auto : dbd:Mysql.dbd -> unit -> unit
val reflexivity : unit -> unit
val symmetry : unit -> unit
val discriminate : Cic.term -> unit
val decide_equality : unit -> unit
val compare : Cic.term -> unit
-
-
-(*
-val prova_tatticali : unit -> unit
-*)