From e11854569b855ae4d675e560d807ec14b8b607bf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 4 Dec 2014 11:38:36 +0100
Subject: Trying a new policy for when to automatically print goals (granting
 the non-verbose mode which I guess one wants to obey whatever interface is
 used, and restoring a policy ok for coqtop - maybe would need a change if
 obeying the local verbose flag is not ok for PG or Jedit).

---
 stm/stm.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 83926adccf..94987bdb91 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2322,10 +2322,10 @@ let interp verb (_,e as lexpr) =
       !Flags.compilation_mode = Flags.BuildVo) then
     let vcs = VCS.backup () in
     let print_goals =
-      (if !Flags.print_emacs then Flags.is_verbose () else !Flags.coqtop_ui) &&
-      match clas with
-      | VtQuery _, _ -> false
-      | _ -> true in
+      verb && match clas with
+       | VtQuery _, _ -> false
+       | VtProofStep _, _ -> true
+       | _ -> not !Flags.coqtop_ui || !Flags.print_emacs in
     try finish ~print_goals ()
     with e ->
       let e = Errors.push e in
-- 
cgit v1.2.3