From a30448fe3b82283e749e009a37bfd4dacb0eaaeb Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 3 Nov 2014 18:51:59 +0100
Subject: Show: do print the goals

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

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ae7f2b1184..ab5cee5cde 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1699,7 +1699,7 @@ let vernac_bullet (bullet:Proof_global.Bullet.t) =
 let vernac_show = function
   | ShowGoal goalref ->
     let info = match goalref with
-      | OpenSubgoals -> mt() (* the STM prints it *)
+      | OpenSubgoals -> pr_open_subgoals ()
       | NthGoal n -> pr_nth_open_subgoal n
       | GoalId id -> pr_goal_by_id id
     in
-- 
cgit v1.2.3