From 0147ba258d67f061386c398c48948810d1efaa64 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 22 Oct 2004 12:54:07 +0000 Subject: [PATCH] auto needs DBI handle --- helm/gTopLevel/invokeTactics.ml | 3 ++- helm/gTopLevel/invokeTactics.mli | 1 + 2 files changed, 3 insertions(+), 1 deletion(-) 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 = -- 2.39.2