]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/tactics/autoTactic.ml
deps fixed
[helm.git] / helm / software / components / tactics / autoTactic.ml
index 12041b2bc28a5354867ee6ca292d580bd48abd72..964959ea9b4092ff134c0449e5e2b5cd0a841d5a 100644 (file)
@@ -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