aboutsummaryrefslogtreecommitdiffstats
path: root/debug/Dwarfgen.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-10-01 19:16:59 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-10-01 19:16:59 +0200
commit2d96b7927719c3b61fe564e8ab273a1b154912a5 (patch)
tree163ebd8697718a117073960b95b8bc343cee02a0 /debug/Dwarfgen.ml
parentbc894f212d478b422f17ca0a0a207833838f173c (diff)
downloadcompcert-kvx-2d96b7927719c3b61fe564e8ab273a1b154912a5.tar.gz
compcert-kvx-2d96b7927719c3b61fe564e8ab273a1b154912a5.zip
Moved the types defined by the Debug Interface into a separate file.
Diffstat (limited to 'debug/Dwarfgen.ml')
-rw-r--r--debug/Dwarfgen.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml
index 6c79ce0c..1ef00c31 100644
--- a/debug/Dwarfgen.ml
+++ b/debug/Dwarfgen.ml
@@ -15,8 +15,10 @@ open C
open Camlcoq
open Cutil
open DebugInformation
+open DebugTypes
open DwarfTypes
open DwarfUtil
+
(* Generate the dwarf DIE's from the information collected in DebugInformation *)
(* Helper function to get values that must be set. *)