diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 31bfc004a8..b6a1a53fa8 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1786,6 +1786,7 @@ let vernac_show = 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 | ShowGoalImplicitly None -> |