X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FinvokeTactics.mli;h=993199fe4b9fa70866297dc9aef8e40a8e79b715;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=41cc917b7bed4ed4fc134a9d5d7735ea525383a9;hpb=fe1e7e151af9690f312259a4c1c969a1388bee5f;p=helm.git

diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli
index 41cc917b7..993199fe4 100644
--- a/helm/gTopLevel/invokeTactics.mli
+++ b/helm/gTopLevel/invokeTactics.mli
@@ -59,6 +59,8 @@ module type Callbacks =
       (UriManager.uri * int * 'a) list ->
       (UriManager.uri * int * 'b list) list
     val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type
+    val mqi_handle : MQIConn.handle
+    val dbd:Mysql.dbd
   end
 
 module type Tactics =
@@ -101,6 +103,7 @@ module type Tactics =
    val whd_in_scratch : unit -> unit
    val reduce_in_scratch : unit -> unit
    val simpl_in_scratch : unit -> unit
+   val auto : unit -> unit  
  end
 
 module Make (C : Callbacks) : Tactics