diff options
| -rw-r--r-- | toplevel/vernac.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 92730c14d..74c7663ca 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -286,7 +286,12 @@ let ensure_exists f = let compile verbosely f = let check_pending_proofs () = let pfs = Proof_global.get_all_proof_names () in - if not (List.is_empty pfs) then vernac_error (str "There are pending proofs") + if not (List.is_empty pfs) then + vernac_error (str "There are pending proofs: " + ++ (pfs + |> List.rev + |> prlist_with_sep pr_comma Names.Id.print) + ++ str ".") in match !Flags.compilation_mode with | BuildVo -> |