From e4f0651516ee7c8bdfd9832aa3afa74e61f9fa81 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
Date: Fri, 9 Jun 2017 15:42:50 +0200
Subject: "There are pending proofs" error message now lists the name of the
 proofs.

This closes https://coq.inria.fr/bugs/show_bug.cgi?id=5275
---
 toplevel/vernac.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'toplevel')

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 ->
-- 
cgit v1.2.3