diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-31 15:49:09 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2015-11-02 15:46:40 +0100 |
| commit | 4e643d134f02cfa9a73754c3cf48048541324834 (patch) | |
| tree | 54a8d34fb69fd23b1d5034f13c2cafb20fcc3e0f /toplevel/vernacentries.ml | |
| parent | 69be6a29cf9f774cb4afe94d76b157ba50984c1d (diff) | |
Adding syntax "Show id" to show goal named id (shelved or not).
Diffstat (limited to 'toplevel/vernacentries.ml')
| -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 31bfc004a..b6a1a53fa 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 -> |