aboutsummaryrefslogtreecommitdiffstats
path: root/arm/AsmToJSON.mli
diff options
context:
space:
mode:
Diffstat (limited to 'arm/AsmToJSON.mli')
-rw-r--r--arm/AsmToJSON.mli8
1 files changed, 6 insertions, 2 deletions
diff --git a/arm/AsmToJSON.mli b/arm/AsmToJSON.mli
index 058a4e83..52c055c4 100644
--- a/arm/AsmToJSON.mli
+++ b/arm/AsmToJSON.mli
@@ -10,6 +10,10 @@
(* *)
(* *********************************************************************)
-val pp_program: Format.formatter -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit
-
val pp_mnemonics: Format.formatter -> unit
+
+val print_if: (Asm.coq_function AST.fundef, 'a) AST.program -> string -> unit
+
+val destination: string option ref
+
+val sdump_folder : string ref