diff options
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f83546ea66..41f63644d4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1853,7 +1853,6 @@ let vernac_show = let open Feedback in function | OpenSubgoals -> pr_open_subgoals () | NthGoal n -> pr_nth_open_subgoal n | GoalId id -> pr_goal_by_id id - | GoalUid id -> pr_goal_by_uid id in msg_notice info | ShowProof -> show_proof () |