diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index ef16df5b75..c0272f2108 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1844,10 +1844,6 @@ let vernac_show = let open Feedback in function | GoalUid id -> pr_goal_by_uid id in msg_notice info - | ShowGoalImplicitly None -> - Constrextern.with_implicits msg_notice (pr_open_subgoals ()) - | ShowGoalImplicitly (Some n) -> - Constrextern.with_implicits msg_notice (pr_nth_open_subgoal n) | ShowProof -> show_proof () | ShowNode -> show_node () | ShowExistentials -> show_top_evars () |