X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FinvokeTactics.mli;h=cf116a5421e2ae665b28c12f078a2232746ebe5e;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=a304e7e3b27efb8005e32f0cd3e96bacc7ddb7ba;hpb=feb3c287997f7d35747c12e0db62e6194f5587a3;p=helm.git

diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli
index a304e7e3b..cf116a542 100644
--- a/helm/gTopLevel/invokeTactics.mli
+++ b/helm/gTopLevel/invokeTactics.mli
@@ -51,8 +51,6 @@ module type Callbacks =
         set_metasenv : Cic.metasenv -> unit ;
         context: Cic.context ;
         set_context : Cic.context -> unit >
-    (* output messages *)
-    val output_html : Ui_logger.html_msg -> unit
     (* GUI refresh functions *)
     val refresh_proof : unit -> unit
     val refresh_goals : unit -> unit
@@ -61,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 dbh : Dbi.connection
   end
 
 module type Tactics =
@@ -103,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