diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml
index 59eb98111..96a09ad91 100644
--- a/src/lsp/lp_doc.ml
+++ b/src/lsp/lp_doc.ml
@@ -71,7 +71,7 @@ let process_pstep (pstate,diags,logs) tac nb_subproofs =
       let goals = Some (current_goals pstate) in
       pstate, (tac_loc, 4, msg, goals) :: diags, logs
       
-      let process_proof pstate tacs logs =
+let process_proof pstate tacs logs =
   Pure.ProofTree.fold process_pstep (pstate,[],logs) tacs
 
 let get_goals dg_proof =