X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FinvokeTactics.mli;h=41cc917b7bed4ed4fc134a9d5d7735ea525383a9;hb=29442b4d21cf07992ad4e5c981085dada1f90fe4;hp=200e50a15535eb69da4044fbc7f766eab9399e0c;hpb=ee35ccaff9728ecba44c83eed9cb703d9a1f131e;p=helm.git

diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli
index 200e50a15..41cc917b7 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
@@ -60,8 +58,7 @@ module type Callbacks =
     val decompose_uris_choice_callback :
       (UriManager.uri * int * 'a) list ->
       (UriManager.uri * int * 'b list) list
-    val mk_fresh_name_callback :
-      Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+    val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type
   end
 
 module type Tactics =