diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-06-09 15:42:50 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-06-16 11:21:07 +0200 |
| commit | e4f0651516ee7c8bdfd9832aa3afa74e61f9fa81 (patch) | |
| tree | 4a946a6643fa3a53ca7461000dd040adff16ce40 /toplevel | |
| parent | 1d3703be3ab41d016c776bb29d9f5eff0cdb401d (diff) | |
"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
Diffstat (limited to 'toplevel')
| -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 -> |