aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-09-14 10:15:49 +0000
committerGravatar regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-09-14 10:15:49 +0000
commit0affc36749655cd0a906af0c0aad64fd350d4fec (patch)
treecdbaaa1fa6f351c69e4906da70490054fb6f13e5
parent20a663fc7c2636833d7c789ca70efebe545df747 (diff)
lib/Pp:
Backtrack on the removal of a type definition. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15799 85f007b7-540e-0410-9357-904b9bb8a0f7
-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