aboutsummaryrefslogtreecommitdiff
path: root/printing/ppvernac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/ppvernac.ml')
-rw-r--r--printing/ppvernac.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 930166524c..b7ac274b7f 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -769,6 +769,7 @@ let rec pr_vernac = function
| VernacSolve (i,tac,deftac) ->
let pr_goal_selector = function
| SelectNth i -> int i ++ str":"
+ | SelectId id -> pr_id id ++ str":"
| SelectAll -> str"all" ++ str":"
| SelectAllParallel -> str"par"
in