diff options
| author | Hugo Herbelin | 2015-10-31 15:49:09 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2015-11-02 15:46:40 +0100 |
| commit | 4e643d134f02cfa9a73754c3cf48048541324834 (patch) | |
| tree | 54a8d34fb69fd23b1d5034f13c2cafb20fcc3e0f /printing/ppvernac.ml | |
| parent | 69be6a29cf9f774cb4afe94d76b157ba50984c1d (diff) | |
Adding syntax "Show id" to show goal named id (shelved or not).
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 00c276bdbe..72b9cafe3f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -594,7 +594,8 @@ module Make let pr_goal_reference = function | OpenSubgoals -> mt () | NthGoal n -> spc () ++ int n - | GoalId n -> spc () ++ str n in + | GoalId id -> spc () ++ pr_id id + | GoalUid n -> spc () ++ str n in let pr_showable = function | ShowGoal n -> keyword "Show" ++ pr_goal_reference n | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n |