diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml
index 4bd40cce8..df92ce330 100644
--- a/src/lsp/lp_doc.ml
+++ b/src/lsp/lp_doc.ml
@@ -65,7 +65,8 @@ let process_pstep (pstate,diags,logs) tac nb_subproofs =
     pstate, (tac_loc, 4, qres, goals) :: diags, logs
   | Tac_Error(loc,msg) ->
     let loc = option_default loc tac_loc in
-    pstate, (loc, 1, msg, None) :: diags, ((1, msg), loc) :: logs
+    let goals = Some (current_goals pstate) in
+    pstate, (loc, 1, msg, goals) :: diags, ((1, msg), loc) :: logs
 
 let process_proof pstate tacs logs =
   Pure.ProofTree.fold process_pstep (pstate,[],logs) tacs