aboutsummaryrefslogtreecommitdiffstats
path: root/debug/DebugInit.ml
diff options
context:
space:
mode:
Diffstat (limited to 'debug/DebugInit.ml')
-rw-r--r--debug/DebugInit.ml6
1 files changed, 0 insertions, 6 deletions
diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml
index 17a90536..24712b27 100644
--- a/debug/DebugInit.ml
+++ b/debug/DebugInit.ml
@@ -10,12 +10,6 @@
(* *)
(* *********************************************************************)
-open AST
-open BinNums
-open C
-open Camlcoq
-open Dwarfgen
-open DwarfTypes
open Debug
let default_debug =