aboutsummaryrefslogtreecommitdiffstats
path: root/arm
diff options
context:
space:
mode:
Diffstat (limited to 'arm')
-rw-r--r--arm/AsmToJSON.ml4
-rw-r--r--arm/AsmToJSON.mli2
2 files changed, 3 insertions, 3 deletions
diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml
index bb0c0c04..73706d3b 100644
--- a/arm/AsmToJSON.ml
+++ b/arm/AsmToJSON.ml
@@ -14,5 +14,5 @@
(* Dummy function *)
-let p_program oc prog =
- ()
+let pp_program pp prog =
+ Format.fprintf pp "null"
diff --git a/arm/AsmToJSON.mli b/arm/AsmToJSON.mli
index 20bcba5e..e4d9c39a 100644
--- a/arm/AsmToJSON.mli
+++ b/arm/AsmToJSON.mli
@@ -10,4 +10,4 @@
(* *)
(* *********************************************************************)
-val p_program: out_channel -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit
+val pp_program: Format.formatter -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit