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

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

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index f986bc867dcf5c1ed61655bc95267fa2a867e1ab..0a7544ef83fcdf5be48cc7e95368bf9e9fe38aa4 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -181,10 +181,10 @@ let new_search_theorems f proof goal depth gtl =
 
 exception NoOtherChoices;;
 
-let rec auto_new dbh = function
+let rec auto_new dbd = function
     [] -> raise NoOtherChoices
   | (proof, [])::tl -> (proof, [])::tl
-  | (proof, (goal,0)::gtl)::tl -> auto_new dbh tl
+  | (proof, (goal,0)::gtl)::tl -> auto_new dbd tl
   | (proof, (goal,depth)::gtl)::tl ->
       let _,metasenv,proof_obj,_ = proof in
       let meta_inf = 
@@ -202,7 +202,7 @@ let rec auto_new dbh = function
                  search_theorems_in_context proof goal (depth-1) gtl in
              let global_choices =
                new_search_theorems 
-                  (fun status -> List.map snd (MetadataQuery.hint ~dbh status))
+                  (fun status -> List.map snd (MetadataQuery.hint ~dbd status))
 (*               (TacticChaser.searchTheorems mqi_handle)  *)
                  proof goal (depth-1) gtl in
              let all_choices =
@@ -216,17 +216,17 @@ let rec auto_new dbh = function
              let reorder = 
                List.stable_sort sorting_list all_choices
              in
-               auto_new dbh reorder
-         | None -> auto_new dbh ((proof,gtl)::tl)
+               auto_new dbd reorder
+         | None -> auto_new dbd ((proof,gtl)::tl)
 ;;
 
 
-let auto_tac ~(dbh:Dbi.connection) =
+let auto_tac ~(dbd:Mysql.dbd) =
 (*   CicMetaSubst.reset_counters (); *)
- let auto_tac dbh (proof,goal) =
+ let auto_tac dbd (proof,goal) =
   prerr_endline "Entro in Auto";
   try 
-    (match auto_new dbh [(proof, [(goal,depth)])] with
+    (match auto_new dbd [(proof, [(goal,depth)])] with
     | (proof,_)::_  ->
       prerr_endline "AUTO_TAC HA FINITO";
   (*     CicMetaSubst.print_counters (); *)
@@ -237,7 +237,7 @@ let auto_tac ~(dbh:Dbi.connection) =
       prerr_endline("Auto failed");
       raise (ProofEngineTypes.Fail "No Applicable theorem")
  in
-  ProofEngineTypes.mk_tactic (auto_tac dbh)
+  ProofEngineTypes.mk_tactic (auto_tac dbd)
 ;;
 
 (* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio