aboutsummaryrefslogtreecommitdiffstats
path: root/arm/PrintAsm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'arm/PrintAsm.ml')
-rw-r--r--arm/PrintAsm.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 16f22d60..f51a15b7 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -14,7 +14,6 @@
open Printf
open Datatypes
-open CList
open Camlcoq
open AST
open Asm