]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/variousTactics.mli
no longer use Dbi module but directly use Mysql module since it's 13
[helm.git] / helm / ocaml / tactics / variousTactics.mli
index ebbf843326b9d9f179b1e133ad6cb41528f9cbb4..5c7c9a0a9a0a8786f1c0fc3e3783475af5c89d12 100644 (file)
@@ -33,5 +33,5 @@ val generalize_tac:
   ProofEngineTypes.tactic
 
 (* val auto_tac : MQIConn.handle -> ProofEngineTypes.tactic *)
-val auto_tac : dbh:Dbi.connection -> ProofEngineTypes.tactic
+val auto_tac : dbd:Mysql.dbd -> ProofEngineTypes.tactic