return goals in previous state instead on None in case of Tactic_error

Alidra · Nov 7, 2024 · 40edfbe · 40edfbe
1 parent d27c7d7
commit 40edfbe
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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