aboutsummaryrefslogtreecommitdiffstats
path: root/backend/JsonAST.mli
diff options
context:
space:
mode:
Diffstat (limited to 'backend/JsonAST.mli')
-rw-r--r--backend/JsonAST.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/JsonAST.mli b/backend/JsonAST.mli
index 7afdce51..c32439e4 100644
--- a/backend/JsonAST.mli
+++ b/backend/JsonAST.mli
@@ -13,4 +13,4 @@
val pp_mnemonics : Format.formatter -> string list -> unit
-val pp_ast : Format.formatter -> (Format.formatter -> Asm.code -> unit) -> (Asm.coq_function AST.fundef, 'a) AST.program -> string -> unit
+val pp_ast : out_channel -> (out_channel -> Asm.code -> unit) -> (Asm.coq_function AST.fundef, 'a) AST.program -> string -> unit