diff --git a/src/plugins/server/data.ml b/src/plugins/server/data.ml
index bdaa0d0c3158856866febda02f142ddcd1b5b644..c3229cdde4a054cfb8912468b514f1538d0ea104 100644
--- a/src/plugins/server/data.ml
+++ b/src/plugins/server/data.ml
@@ -593,6 +593,7 @@ sig
   val empty : 'a t
   val add : key -> 'a -> 'a t -> 'a t
   val find : key -> 'a t -> 'a
+  val remove : key -> 'a t -> 'a t
 end
 
 module type Index =
@@ -601,6 +602,7 @@ sig
   type tag
   val get : t -> tag
   val find : tag -> t
+  val remove : t -> unit
   val clear : unit -> unit
 end
 
@@ -611,6 +613,7 @@ sig
   val clear : index -> unit
   val get : index -> M.key -> int
   val find : index -> int -> M.key
+  val remove : index -> M.key -> unit
   val to_json : index -> M.key -> json
   val of_json : index -> json -> M.key
 end =
@@ -643,6 +646,13 @@ struct
       m.index <- M.add a id m.index ;
       Hashtbl.add m.lookup id a ; id
 
+  let remove m a =
+    try
+      let id = M.find a m.index in
+      Hashtbl.remove m.lookup id ;
+      m.index <- M.remove a m.index ;
+    with Not_found -> ()
+
   let find m id = Hashtbl.find m.lookup id
 
   let to_json m a = `Int (get m a)
@@ -662,6 +672,7 @@ struct
   let clear () = INDEX.clear index
   let get = INDEX.get index
   let find = INDEX.find index
+  let remove = INDEX.remove index
   include
     (struct
       type t = M.key
@@ -694,6 +705,7 @@ struct
 
   let index () = STATE.get ()
   let clear () = INDEX.clear (index())
+  let remove a = INDEX.remove (index()) a
 
   let get a = INDEX.get (index()) a
   let find id = INDEX.find (index()) id
@@ -761,6 +773,11 @@ struct
     let hash = lookup () in
     if not (Hashtbl.mem hash tag) then Hashtbl.add hash tag x ; tag
 
+  let remove x =
+    let tag = A.id x in
+    let hash = lookup () in
+    Hashtbl.remove hash tag
+
   include
     (struct
       type t = A.t
diff --git a/src/plugins/server/data.mli b/src/plugins/server/data.mli
index c9fe14a36a55800db6d21a507ce99a6cf9d3d637..36a02e94a652e4255a27648b4034323a1bc0dd55 100644
--- a/src/plugins/server/data.mli
+++ b/src/plugins/server/data.mli
@@ -357,6 +357,7 @@ sig
   val empty : 'a t
   val add : key -> 'a -> 'a t -> 'a t
   val find : key -> 'a t -> 'a
+  val remove : key -> 'a t -> 'a t
 end
 
 (** Datatype extended with access to value identifiers. *)
@@ -368,6 +369,9 @@ sig
   val find : tag -> t
   (** @raise Not_found if not registered. *)
 
+  val remove : t -> unit
+  (** Remove item from index tables. Use with extreme care. *)
+
   val clear : unit -> unit
   (** Clear index tables. Use with extreme care. *)
 end
diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index c1398c17a5c2148b57a862542b266a8e04bce733..1d223fd08645405c86b9b5d1a3e092fe2be1861b 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -113,6 +113,12 @@ let set_saved t s = t.saved <- s
 (* --- Removal                                                            --- *)
 (* -------------------------------------------------------------------------- *)
 
+let clear_hooks = ref []
+let remove_hooks = ref []
+
+let add_clear_hook fn = clear_hooks := !clear_hooks @ [fn]
+let add_remove_hook fn = remove_hooks := !remove_hooks @ [fn]
+
 let rec revert_tactic t n =
   n.strategy <- None ;
   match n.script with
@@ -125,15 +131,13 @@ and remove_node t n =
     Wpo.remove n.goal
   else
     Wpo.clear_results n.goal ;
-  begin
-    match t.head with
-    | Some n0 when n0 == n -> t.head <- None
-    | _ -> ()
-  end ;
+  List.iter (fun f -> f n) !remove_hooks ;
+  Option.iter (fun n0 -> if n0 == n then t.head <- None) t.head ;
   revert_tactic t n
 
 let clear_tree t =
   begin
+    List.iter (fun f -> f ()) !clear_hooks ;
     Wpo.clear_results t.main ;
     Option.iter (remove_node t) t.root ;
     t.gid <- 0 ;
diff --git a/src/plugins/wp/ProofEngine.mli b/src/plugins/wp/ProofEngine.mli
index 31931dcb6cf284e1f28b05963108adfb512694f6..7e57c95aabc91df4c257a81323105ca503793b75 100644
--- a/src/plugins/wp/ProofEngine.mli
+++ b/src/plugins/wp/ProofEngine.mli
@@ -101,6 +101,8 @@ val clear_tree : tree -> unit
 val clear_node : tree -> node -> unit
 val clear_node_tactic : tree -> node -> unit
 val clear_parent_tactic : tree -> node -> unit
+val add_clear_hook : (unit -> unit) -> unit
+val add_remove_hook : (node -> unit) -> unit
 
 val cancel_parent_tactic : tree -> unit
 val cancel_current_node : tree -> unit
diff --git a/src/plugins/wp/wpTipApi.ml b/src/plugins/wp/wpTipApi.ml
index 46d2716b89ba9d7443cf3755778f46abf479ad24..6e56e120d90d21428bf2ca2ad0bb14873d0dd5cc 100644
--- a/src/plugins/wp/wpTipApi.ml
+++ b/src/plugins/wp/wpTipApi.ml
@@ -59,6 +59,12 @@ module Node = D.Index
       let descr = Md.plain "Proof Node index"
     end)
 
+let () = Server.Main.once
+    begin fun () ->
+      ProofEngine.add_clear_hook Node.clear ;
+      ProofEngine.add_remove_hook Node.remove ;
+    end
+
 module Tactic : D.S with type t = Tactical.t =
 struct
   type t = Tactical.t