diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml
index 69d5e646b..59eb98111 100644
--- a/src/lsp/lp_doc.ml
+++ b/src/lsp/lp_doc.ml
@@ -69,7 +69,7 @@ let process_pstep (pstate,diags,logs) tac nb_subproofs =
       pstate, (loc, 1, msg, None) :: diags, ((1, msg), loc) :: logs
     | Some pstate -> 
       let goals = Some (current_goals pstate) in
-      pstate, (tac_loc, 4, "qres", goals) :: diags, logs
+      pstate, (tac_loc, 4, msg, goals) :: diags, logs
       
       let process_proof pstate tacs logs =
   Pure.ProofTree.fold process_pstep (pstate,[],logs) tacs
diff --git a/src/pure/pure.ml b/src/pure/pure.ml
index bfb923a9e..8b38beb29 100644
--- a/src/pure/pure.ml
+++ b/src/pure/pure.ml
@@ -170,8 +170,7 @@ let handle_tactic : proof_state -> Tactic.t -> int -> tactic_result =
   | Fatal(Some p,m) ->
     Tac_Error(None , Some p, Pos.popt_to_string p ^ m)
   | Handle.Tactic.Tactic_error(a, Some p,m) ->
-    let ps, qres = a in
-    let _qres = Option.map (fun f -> f ()) qres in
+    let ps, _qres = a in
     Tac_Error(Some (Time.save (), ss, ps, finalize, prv, sym_pos), Some p, Pos.popt_to_string p ^ m)
 
 let end_proof : proof_state -> command_result =