diff options
| author | Maxime Dénès | 2017-04-14 14:02:10 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-14 14:02:10 +0200 |
| commit | 144f032a416a0701f3183c156769f30e64362549 (patch) | |
| tree | 9e0327ba26213a81ab85236583adee8d3c2c9be7 | |
| parent | fd197553c11bc968aa13b9db6a49608b5d8accc4 (diff) | |
| parent | 041cb0de6204989000352311e01847ce5a908a14 (diff) | |
Merge PR#557: [toplevel] Don't print goals if there is no pending proof.
| -rw-r--r-- | toplevel/vernac.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 98458a57a2..18f93197c1 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -126,11 +126,12 @@ let rec interp_vernac sid po (loc,com) = (* Stm.observe nsid; *) Stm.finish (); - (* We could use a more refined criteria depending on the + (* We could use a more refined criteria that depends on the vernac. For now we imitate the old approach. *) - let print_goals = not (!Flags.batch_mode || is_query v) in + let hide_goals = !Flags.batch_mode || is_query v || + not (Proof_global.there_are_pending_proofs ()) in - if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); + if not hide_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); nsid with exn when CErrors.noncritical exn -> |