aboutsummaryrefslogtreecommitdiffstats
path: root/arm/PrintAsm.mli
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2015-03-10 14:30:00 +0100
committerXavier Leroy <xavierleroy@users.noreply.github.com>2015-03-10 14:30:00 +0100
commit337dddf6ea7c69c06c883ce4287ddf3d92b63c05 (patch)
tree92ceb94ef94aff3fe22ce11bb21452341f2dd717 /arm/PrintAsm.mli
parent3e01154d693e1c457e1e974f5e9ebaa4601050aa (diff)
parent5a027c08f3fed3e52061978e1757ffb255422333 (diff)
downloadcompcert-337dddf6ea7c69c06c883ce4287ddf3d92b63c05.tar.gz
compcert-337dddf6ea7c69c06c883ce4287ddf3d92b63c05.zip
Merge pull request #21 from AbsInt/backend_printer
Re-factoring of the asm printers.
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