fix hover message in case of problem with the number of subproofs

Alidra · Oct 24, 2024 · 037f74a · 037f74a
1 parent 11d6b5c
commit 037f74a
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 3 deletions.
diff --git 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
@@ -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 =