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

diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli
index 41cc917b7..5578c43e5 100644
--- a/helm/gTopLevel/invokeTactics.mli
+++ b/helm/gTopLevel/invokeTactics.mli
@@ -59,6 +59,7 @@ 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
   end
 
 module type Tactics =
@@ -101,6 +102,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