diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-04-23 14:06:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-04-23 14:06:19 +0200 |
| commit | 0a2dfa5e5d17ccf58328432888dff345ef0bf5e6 (patch) | |
| tree | 263444a0609afaac00284ad8d367eb561d4676c1 /lib/pp.mli | |
| parent | 501d6dd5691474c807a722d9b5b6e3fa9d83c749 (diff) | |
Removing dead code in Pp.
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index 5dd2686d1..e20e5ca82 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -46,9 +46,6 @@ 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 |