New module HMysql (to abstract over Mysql and make profiling easier).

[helm.git] / helm / ocaml / tactics / autoTactic.ml

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index e89608cd4f9c04438b3e1e7d2f823f5efeb11c64..a0835a9b89db982e12e2a483cda54c72afa29068 100644 (file)
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -279,7 +279,7 @@ let default_depth = 5
 let default_width = 3
 
 (*
-let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd)
+let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
   ()
 =
   let auto_tac dbd (proof,goal) =
@@ -311,7 +311,7 @@ let term_is_equality = ref
   (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);;
 
 
-let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ~(dbd:Mysql.dbd) () =
+let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ~(dbd:HMysql.dbd) () =
   let auto_tac dbd (proof, goal) =
     let normal_auto () = 
       let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in