From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 22 Oct 2004 12:54:07 +0000 (+0000)
Subject: auto needs DBI handle
X-Git-Tag: V_0_0_10~27
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0147ba258d67f061386c398c48948810d1efaa64;p=helm.git

auto needs DBI handle
---

diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index e96928988..ecacc9b7c 100644
--- a/helm/gTopLevel/invokeTactics.ml
+++ b/helm/gTopLevel/invokeTactics.ml
@@ -62,6 +62,7 @@ module type Callbacks =
       (UriManager.uri * int * 'b list) list
     val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type
     val mqi_handle : MQIConn.handle
+    val dbh: Dbi.connection
   end
 ;;
 
@@ -305,7 +306,7 @@ module Make (C: Callbacks) : Tactics =
     (ProofEngine.intros ~mk_fresh_name_callback:C.mk_fresh_name_callback)
   let exact = call_tactic_with_input ProofEngine.exact
   let apply = call_tactic_with_input ProofEngine.apply
-  let auto = call_tactic (ProofEngine.auto C.mqi_handle)
+  let auto = call_tactic (ProofEngine.auto C.dbh)
   let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl
   let elimtype = call_tactic_with_input ProofEngine.elim_type
   let whd = call_tactic_with_goal_inputs ProofEngine.whd
diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli
index 5578c43e5..cf116a542 100644
--- a/helm/gTopLevel/invokeTactics.mli
+++ b/helm/gTopLevel/invokeTactics.mli
@@ -60,6 +60,7 @@ module type Callbacks =
       (UriManager.uri * int * 'b list) list
     val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type
     val mqi_handle : MQIConn.handle
+    val dbh : Dbi.connection
   end
 
 module type Tactics =