diff options
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index dafbc3d820..7420f2784e 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1276,13 +1276,8 @@ end) = struct include Make (Ppconstr.RichPp (Indexer)) (struct open Ppannotation - - let tag_keyword t = - Pp.open_tag (Indexer.index AKeyword) ++ t ++ Pp.close_tag () - - let tag_vernac v t = - Pp.open_tag (Indexer.index (AVernac v)) ++ t ++ Pp.close_tag () - + let tag_keyword = Pp.tag (Indexer.index AKeyword) + let tag_vernac v = Pp.tag (Indexer.index (AVernac v)) end) end |