lib/Pp.tag: New.

   A combinator to introduce tags.
printing/{Ppconstr, Ppvernac}: Use it.

1 files changed, 1 insertions, 1 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index b8935f54dc..c47d638337 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -217,7 +217,7 @@ let tclose () = Glue.atom(Ppcmd_close_tbox)
 (* Opening and closed of tags *)
 let open_tag t = Glue.atom(Ppcmd_open_tag t)
 let close_tag () = Glue.atom(Ppcmd_close_tag)
-
+let tag t s = open_tag t ++ s ++ close_tag ()
 let eval_ppcmds l = l
 
 (* In new syntax only double quote char is escaped by repeating it *)