new getter, logger, and the hell

[helm.git] / helm / gTopLevel / invokeTactics.mli

diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli
index a304e7e3b27efb8005e32f0cd3e96bacc7ddb7ba..41cc917b7bed4ed4fc134a9d5d7735ea525383a9 100644 (file)
--- 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