aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--lib/pp.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/lib/pp.ml b/lib/pp.ml
index 1899b2d3c..5a38b08c3 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -71,6 +71,8 @@ type ppcmd = (int*string) ppcmd_token
type std_ppcmds = ppcmd Stream.t
+type 'a ppdirs = 'a ppdir_token Stream.t
+
let is_empty s =
try Stream.empty s; true with Stream.Failure -> false
@@ -282,7 +284,7 @@ let pp_dirs ft =
com_brk ft; Format.pp_print_newline ft ()
| Ppdir_print_flush -> Format.pp_print_flush ft ()
in
- fun dirstream ->
+ fun (dirstream : _ ppdirs) ->
try
Stream.iter pp_dir dirstream; com_brk ft
with