no longer use Dbi module but directly use Mysql module since it's 13

[helm.git] / helm / gTopLevel / invokeTactics.ml

diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index ecacc9b7c503a911d5bea34b2b5bda94f1c79b94..cbe25219ce724b58c807c2aeae72cf2e62e0d9cc 100644 (file)
--- a/helm/gTopLevel/invokeTactics.ml
+++ b/helm/gTopLevel/invokeTactics.ml
@@ -62,7 +62,7 @@ module type Callbacks =
       (UriManager.uri * int * 'b list) list
     val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type
     val mqi_handle : MQIConn.handle
-    val dbh: Dbi.connection
+    val dbd:Mysql.dbd
   end
 ;;
 
@@ -306,7 +306,7 @@ module Make (C: Callbacks) : Tactics =
     (ProofEngine.intros ~mk_fresh_name_callback:C.mk_fresh_name_callback)
   let exact = call_tactic_with_input ProofEngine.exact
   let apply = call_tactic_with_input ProofEngine.apply
-  let auto = call_tactic (ProofEngine.auto C.dbh)
+  let auto = call_tactic (ProofEngine.auto ~dbd:C.dbd)
   let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl
   let elimtype = call_tactic_with_input ProofEngine.elim_type
   let whd = call_tactic_with_goal_inputs ProofEngine.whd