X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FautoTactic.ml;h=964959ea9b4092ff134c0449e5e2b5cd0a841d5a;hb=e1f0bb910f75b8b21f2c5e394ebb4c5a63ef4945;hp=12041b2bc28a5354867ee6ca292d580bd48abd72;hpb=c6cc2a7227d6750076f591a62d7b1896ebf1ebfa;p=helm.git

diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml
index 12041b2bc..964959ea9 100644
--- a/helm/software/components/tactics/autoTactic.ml
+++ b/helm/software/components/tactics/autoTactic.ml
@@ -270,7 +270,7 @@ and auto_new_aux dbd width already_seen_goals universe = function
 let default_depth = 5
 let default_width = 3
 
-let auto_tac_old ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
+let auto_tac_old ?(depth=default_depth) ?(width=default_width) ~(dbd:HSql.dbd)
   ()
 =
   let auto_tac dbd (proof,goal) =
@@ -318,7 +318,7 @@ let int params name default =
         raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
 ;;  
 
-let auto_tac ~params ~(dbd:HMysql.dbd) ~universe (proof, goal) =
+let auto_tac ~params ~(dbd:HSql.dbd) ~universe (proof, goal) =
   (* argument parsing *)
   let int = int params in
   let bool = bool params in