diff options
| author | Maxime Dénès | 2017-06-19 08:44:00 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-19 08:44:00 +0200 |
| commit | 998322deaf0d87ae7f24c12ecacd672941528f78 (patch) | |
| tree | 47ce0c2d896a1e58d45e647f6e3a8f9cd3c40d7d | |
| parent | 52ab54dc6734319203442f36de4d7ddd4fd999b9 (diff) | |
| parent | e4f0651516ee7c8bdfd9832aa3afa74e61f9fa81 (diff) | |
Merge PR#755: "There are pending proofs" error message now lists the name of the proofs.
| -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 92730c14d0..74c7663ca5 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 -> |