From 99c92fedebf629549eb16feb266f55c83ad99bd9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 16 Feb 2017 13:43:38 +0100
Subject: [stm] remove tactic_being_run hook

`tactic_being_run_hook` was used for the "xml" pluging but I am not
sure we have a sensible use case here.
---
 stm/stm.ml  | 12 ++----------
 stm/stm.mli |  3 ---
 2 files changed, 2 insertions(+), 13 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index b0ad3f8790..d505168446 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -52,9 +52,6 @@ let parse_error, parse_error_hook = Hook.make
 let unreachable_state, unreachable_state_hook = Hook.make
  ~default:(fun _ _ -> ()) ()
 
-let tactic_being_run, tactic_being_run_hook = Hook.make
- ~default:(fun _ -> ()) ()
-
 include Hook
 
 (* enables:  Hooks.(call foo args) *)
@@ -2213,10 +2210,8 @@ let known_state ?(redefine_qed=false) ~cache id =
           (fun () ->
             resilient_tactic id cblock (fun () ->
               reach ~cache:`Shallow view.next;
-              Hooks.(call tactic_being_run true); 
               Partac.vernac_interp ~solve ~abstract
-                cancel !Flags.async_proofs_n_tacworkers view.next id x;
-              Hooks.(call tactic_being_run false))
+                cancel !Flags.async_proofs_n_tacworkers view.next id x)
           ), cache, true
       | `Cmd { cast = x; cqueue = `QueryQueue cancel }
         when Flags.async_proofs_is_master () -> (fun () ->
@@ -2226,9 +2221,7 @@ let known_state ?(redefine_qed=false) ~cache id =
       | `Cmd { cast = x; ceff = eff; ctac = true; cblock } -> (fun () ->
             resilient_tactic id cblock (fun () ->
               reach view.next;
-              Hooks.(call tactic_being_run true); 
-              stm_vernac_interp id x;
-              Hooks.(call tactic_being_run false)); 
+              stm_vernac_interp id x);
 	    if eff then update_global_env ()
           ), (if eff then `Yes else cache), true
       | `Cmd { cast = x; ceff = eff } -> (fun () ->
@@ -2946,5 +2939,4 @@ let forward_feedback_hook = Hooks.forward_feedback_hook
 let process_error_hook = Hooks.process_error_hook
 let unreachable_state_hook = Hooks.unreachable_state_hook
 let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref)
-let tactic_being_run_hook = Hooks.tactic_being_run_hook
 (* vim:set foldmethod=marker: *)
diff --git a/stm/stm.mli b/stm/stm.mli
index 0f0a3c4e13..9ae78e02cf 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -187,9 +187,6 @@ val parse_error_hook :
 val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t
 (* ready means that master has it at hand *)
 val state_ready_hook : (Stateid.t -> unit) Hook.t
-(* called with true before and with false after a tactic explicitly
- * in the document is run *)
-val tactic_being_run_hook : (bool -> unit) Hook.t
 
 (* Messages from the workers to the master *)
 val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t
-- 
cgit v1.2.3