summaryrefslogtreecommitdiff
path: root/src/pretty_print.mli
diff options
context:
space:
mode:
authorGabriel Kerneis2014-05-15 16:46:31 +0100
committerGabriel Kerneis2014-05-15 16:46:31 +0100
commitf09fc91feadd58481402c940a728bdda84aecb14 (patch)
treed6261dd4d37ac5d73265527b7ef3bd196889400f /src/pretty_print.mli
parent5a23af520ddd3dedd9d5c4d7aeab5c5d6f2a7a4f (diff)
Make pp_exp export to buffer
Diffstat (limited to 'src/pretty_print.mli')
-rw-r--r--src/pretty_print.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/pretty_print.mli b/src/pretty_print.mli
index 49c4af27..3fdf7841 100644
--- a/src/pretty_print.mli
+++ b/src/pretty_print.mli
@@ -1,9 +1,9 @@
open Ast
open Type_internal
-(* Prints on formatter the defs following source syntax *)
+(* Prints the defs following source syntax *)
val pp_defs : out_channel -> tannot defs -> unit
-val pp_exp : out_channel -> exp -> unit
+val pp_exp : Buffer.t -> exp -> unit
(* Prints on formatter the defs as Lem Ast nodes *)
val pp_lem_defs : Format.formatter -> tannot defs -> unit