From 5b05d3668571bd9b748b781b0cc29ae10f745f61 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 10 Mar 2016 13:35:48 +0100
Subject: Code cleanup.

Removed some unused variables, functions etc. and resolved some
problems which occur if all warnings except 3,4,9 and 29 are active.
Bug 18394.
---
 debug/DebugInit.ml | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'debug/DebugInit.ml')

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 =
-- 
cgit