X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FinvokeTactics.ml;h=31804290930e10986ab38194c8a709e3bdc9a2b6;hb=c2809aab05acc486084279fa04fd63b10575c35a;hp=775d6a4680c36eb49b55533ace7b148332378dd9;hpb=458d0fc95ae3f3a20bd91e3e29ddeb92a009d0fa;p=helm.git

diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index 775d6a468..318042909 100644
--- a/helm/gTopLevel/invokeTactics.ml
+++ b/helm/gTopLevel/invokeTactics.ml
@@ -62,8 +62,6 @@ module type Callbacks =
       (UriManager.uri * int * 'b list) list
     val mk_fresh_name_callback :
       Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
-    (* invoked when the proof assistant's status has changed to notify Hbugs *)
-    val notify_hbugs : unit -> unit
   end
 ;;
 
@@ -119,8 +117,7 @@ module Make (C: Callbacks) : Tactics =
       try
        tactic () ;
        C.refresh_goals () ;
-       C.refresh_proof () ;
-       C.notify_hbugs ()
+       C.refresh_proof ()
       with
          RefreshSequentException e ->
           C.output_html
@@ -172,8 +169,7 @@ module Make (C: Callbacks) : Tactics =
          tactic expr ;
          C.refresh_goals () ;
          C.refresh_proof () ;
-         (C.term_editor ())#reset ;
-         C.notify_hbugs ()
+         (C.term_editor ())#reset
        with
           RefreshSequentException e ->
            C.output_html
@@ -207,8 +203,7 @@ module Make (C: Callbacks) : Tactics =
           try
            tactic term ;
            C.refresh_goals () ;
-           C.refresh_proof () ;
-           C.notify_hbugs ()
+           C.refresh_proof ()
           with
              RefreshSequentException e ->
               C.output_html
@@ -252,7 +247,6 @@ module Make (C: Callbacks) : Tactics =
           tactic terms ;
           C.refresh_goals () ;
           C.refresh_proof () ;
-          C.notify_hbugs ()
      with
         RefreshSequentException e ->
          C.output_html
@@ -304,8 +298,7 @@ module Make (C: Callbacks) : Tactics =
              tactic ~goal_input:term ~input:expr ;
              C.refresh_goals () ;
              C.refresh_proof () ;
-             (C.term_editor ())#reset ;
-             C.notify_hbugs ()
+             (C.term_editor ())#reset
           with
              RefreshSequentException e ->
               C.output_html
@@ -391,8 +384,7 @@ module Make (C: Callbacks) : Tactics =
           try
            tactic hypothesis ;
            C.refresh_goals () ;
-           C.refresh_proof () ;
-           C.notify_hbugs ()
+           C.refresh_proof ()
           with
              RefreshSequentException e ->
               C.output_html