let elim_type term = apply_tactic (EliminationTactics.elim_type_tac ~term)
let ring () = apply_tactic Ring.ring_tac
let fourier () = apply_tactic FourierR.fourier_tac
-let auto mqi_handle () = apply_tactic (VariousTactics.auto_tac mqi_handle)
+let auto dbh () = apply_tactic (VariousTactics.auto_tac ~dbh)
let rewrite_simpl term = apply_tactic (EqualityTactics.rewrite_simpl_tac ~term)
let rewrite_back_simpl term = apply_tactic (EqualityTactics.rewrite_back_simpl_tac ~term)
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 : MQIConn.handle -> unit -> unit
+(* val auto : MQIConn.handle -> unit -> unit *)
+val auto : Dbi.connection -> unit -> unit
val reflexivity : unit -> unit
val symmetry : unit -> unit