From 3e5b9ab9f75e4102068230769861fc875be0e306 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 6 Dec 2014 15:51:40 +0100
Subject: Improving e11854569b8 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 94987bdb91..6babc3e42f 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2324,7 +2324,7 @@ let interp verb (_,e as lexpr) =
     let print_goals =
       verb && match clas with
        | VtQuery _, _ -> false
-       | VtProofStep _, _ -> true
+       | (VtProofStep _ | VtStm (VtBack _, _)), _ -> true
        | _ -> not !Flags.coqtop_ui || !Flags.print_emacs in
     try finish ~print_goals ()
     with e ->
-- 
cgit v1.2.3