diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-01 19:16:59 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-01 19:16:59 +0200 |
commit | 2d96b7927719c3b61fe564e8ab273a1b154912a5 (patch) | |
tree | 163ebd8697718a117073960b95b8bc343cee02a0 /debug/Dwarfgen.ml | |
parent | bc894f212d478b422f17ca0a0a207833838f173c (diff) | |
download | compcert-2d96b7927719c3b61fe564e8ab273a1b154912a5.tar.gz compcert-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.ml | 2 |
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. *) |