diff options
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index eb847189a3..f29f9b2f3b 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -82,6 +82,7 @@ val tclose : unit -> std_ppcmds (** {6 Opening and closing of tags} *) +val tag : string -> std_ppcmds -> std_ppcmds val open_tag : string -> std_ppcmds val close_tag : unit -> std_ppcmds |