diff options
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |