diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml
index 4c6e56d7a3886076076f05564793cc02d872ef05..3807e11851f497b14fb7db102997dc0833bf7b9a 100644
--- a/src/session/itp_server.ml
+++ b/src/session/itp_server.ml
@@ -1312,6 +1312,7 @@ end
     | Some any ->
       let unproven_any =
         get_first_unproven_goal_around
+          ~always_send:false
           ~proved:(Session_itp.any_proved s)
           ~children:(get_undetached_children_no_pa s)
           ~get_parent:(get_any_parent s)
diff --git a/src/session/server_utils.ml b/src/session/server_utils.ml
index f830839686040ca642474cbd667522f12c1ad3b2..4f90c6f86e63da61937caf08f9ccb490aed55a94 100644
--- a/src/session/server_utils.ml
+++ b/src/session/server_utils.ml
@@ -485,7 +485,7 @@ let split_list l node =
   split_list l []
 
 let get_first_unproven_goal_around
-    ~proved ~children ~get_parent ~is_goal ~is_pa node =
+    ~always_send ~proved ~children ~get_parent ~is_goal ~is_pa node =
   let rec look_around node =
     match get_parent node with
     | None -> unproven_goals_below_node ~proved ~children ~is_goal [] node
@@ -505,7 +505,7 @@ let get_first_unproven_goal_around
   | [] ->
     begin
       match before_node with
-      | [] -> None
+      | [] -> if always_send then Some node else None
       | hd :: _tl -> Some hd
     end
   | hd :: _tl  -> Some hd
diff --git a/src/session/server_utils.mli b/src/session/server_utils.mli
index ba06b1a885b3e222bf0c5b42e1bca5513bbfbff0..a44e3dba4949dfaa15fc6ed8957f83df4621af17 100644
--- a/src/session/server_utils.mli
+++ b/src/session/server_utils.mli
@@ -83,10 +83,19 @@ val interp:
   Controller_itp.controller ->
   Session_itp.any option -> string -> command
 
-
+(* Find the first unproven goal around the node given.
+   @param always_send: if true then always returns something
+   @param proved     : oracle for proved node
+   @param children   : returns the list children of a node
+   @param get_parent : returns the parent of a node
+   @param is_goal    : answer true iff a given node is a goal
+   @param is_pa      : answer true iff a given node is a proof attempt
+   @param node       : node_id
+*)
 val get_first_unproven_goal_around:
-    proved:('a -> bool) ->
-      children:('a -> 'a list) ->
-        get_parent:('a -> 'a option) ->
-          is_goal:('a -> bool) ->
-            is_pa:('a -> bool) -> 'a -> 'a option
+    always_send:bool ->
+      proved:('a -> bool) ->
+        children:('a -> 'a list) ->
+          get_parent:('a -> 'a option) ->
+            is_goal:('a -> bool) ->
+              is_pa:('a -> bool) -> 'a -> 'a option