aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-04-24 17:16:59 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-04-24 17:16:59 +0200
commite57074289193b0f0184f3c7143d8ab7e0edd5112 (patch)
tree805ec4ad48d8aeaf0cf5beb742ba734b0c24509f /toplevel/vernac.ml
parent7c11c9a5722f6e205dfb158cf21267db123dd06c (diff)
parenta821f74dc91e438c86037d1dc8903a49934e6ee5 (diff)
Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.
Diffstat (limited to 'toplevel/vernac.ml')
-rw-r--r--toplevel/vernac.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 84330b88a..3359a1672 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -116,7 +116,7 @@ let rec interp_vernac sid po (loc,com) =
load_vernac verbosely sid f
| v ->
try
- let nsid, ntip = Stm.add sid (Flags.is_verbose()) (loc,v) in
+ let nsid, ntip = Stm.add sid (not !Flags.quiet) (loc,v) in
(* Main STM interaction *)
if ntip <> `NewTip then
@@ -128,7 +128,7 @@ let rec interp_vernac sid po (loc,com) =
(* We could use a more refined criteria that depends on the
vernac. For now we imitate the old approach. *)
- let hide_goals = !Flags.batch_mode || is_query v ||
+ let hide_goals = !Flags.batch_mode || is_query v || !Flags.quiet ||
not (Proof_global.there_are_pending_proofs ()) in
if not hide_goals then Feedback.msg_notice (pr_open_cur_subgoals ());