diff options
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index dad4ed6ab..eb847189a 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -46,6 +46,9 @@ val eval_ppcmds : std_ppcmds -> std_ppcmds val is_empty : std_ppcmds -> bool (** Test emptyness. *) +val rewrite : (string -> string) -> std_ppcmds -> std_ppcmds +(** [rewrite f pps] applies [f] to all strings that appear in [pps]. *) + (** {6 Derived commands} *) val spc : unit -> std_ppcmds |