aboutsummaryrefslogtreecommitdiffstats
path: root/arm/PrintAsm.mli
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-02-09 14:54:42 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-02-09 14:54:42 +0100
commita3c0094508f9f4985de4509380dada5f5c85e115 (patch)
tree5d3758130d08ae008e87454dadf603780612b830 /arm/PrintAsm.mli
parentaaec016c81c062ad821fc6a6b8f000308ffaad7f (diff)
downloadcompcert-kvx-a3c0094508f9f4985de4509380dada5f5c85e115.tar.gz
compcert-kvx-a3c0094508f9f4985de4509380dada5f5c85e115.zip
Changed arm backend to the common backend printer.
Diffstat (limited to 'arm/PrintAsm.mli')
-rw-r--r--arm/PrintAsm.mli13
1 files changed, 0 insertions, 13 deletions
diff --git a/arm/PrintAsm.mli b/arm/PrintAsm.mli
deleted file mode 100644
index aefe3a0a..00000000
--- a/arm/PrintAsm.mli
+++ /dev/null
@@ -1,13 +0,0 @@
-(* *********************************************************************)
-(* *)
-(* The Compcert verified compiler *)
-(* *)
-(* Xavier Leroy, INRIA Paris-Rocquencourt *)
-(* *)
-(* Copyright Institut National de Recherche en Informatique et en *)
-(* Automatique. All rights reserved. This file is distributed *)
-(* under the terms of the INRIA Non-Commercial License Agreement. *)
-(* *)
-(* *********************************************************************)
-
-val print_program: out_channel -> Asm.program -> unit