aboutsummaryrefslogtreecommitdiffstats
path: root/backend/JsonAST.mli
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2018-01-05 16:51:32 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2018-01-05 16:51:32 +0100
commit94c18ad233b9e16ee9263ba8b717630b4adbf91e (patch)
treef2e10ea75c79137c78021bc01dca112e9b430c7f /backend/JsonAST.mli
parent91601d4bd435efdee12e08188573f0e9bd910a8a (diff)
downloadcompcert-94c18ad233b9e16ee9263ba8b717630b4adbf91e.tar.gz
compcert-94c18ad233b9e16ee9263ba8b717630b4adbf91e.zip
Change AsmToJson to be similar to other printers.
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 c6fd80c9..7afdce51 100644
--- a/backend/JsonAST.mli
+++ b/backend/JsonAST.mli
@@ -12,5 +12,5 @@
-val pp_program : Format.formatter -> (Format.formatter -> Asm.code -> unit) -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit
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