From f804e681f1550e1c20b8ce5b83bc66c876fb3c99 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 8 Feb 2015 10:20:39 +0100
Subject: Improving further e11854569b8 and 3e5b9ab9f75e4 on when to print
 goals in coqtop mode.

---
 stm/stm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 3a57d85bab..96a11d306d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2278,7 +2278,7 @@ let interp verb (_,e as lexpr) =
     let print_goals =
       verb && match clas with
        | VtQuery _, _ -> false
-       | (VtProofStep _ | VtStm (VtBack _, _)), _ -> true
+       | (VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _), _ -> true
        | _ -> not !Flags.coqtop_ui || !Flags.print_emacs in
     try finish ~print_goals ()
     with e ->
-- 
cgit v1.2.3