aboutsummaryrefslogtreecommitdiffstats
path: root/debug/DwarfTypes.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-03-16 14:51:00 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-03-16 14:51:00 +0100
commit9699d81b304414534008258c05d391bdc1c9e217 (patch)
treea9d1176538486e3f5d26c67ee763d490b1efd23d /debug/DwarfTypes.ml
parent538e8515a6eb1efa8cba3a71456d05f4617999f3 (diff)
downloadcompcert-9699d81b304414534008258c05d391bdc1c9e217.tar.gz
compcert-9699d81b304414534008258c05d391bdc1c9e217.zip
Added printers for the rest of the possible tags.
Diffstat (limited to 'debug/DwarfTypes.ml')
-rw-r--r--debug/DwarfTypes.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/debug/DwarfTypes.ml b/debug/DwarfTypes.ml
index 81c4b858..268711b3 100644
--- a/debug/DwarfTypes.ml
+++ b/debug/DwarfTypes.ml
@@ -70,7 +70,7 @@ type dw_tag_compile_unit =
type dw_tag_const_type =
{
- const_type: reference;
+ const_type: reference;
}
type dw_tag_enumeration_type =
@@ -219,7 +219,7 @@ type dw_tag =
(* The type of the entries. *)
-type dw_entry =
+type dw_entry =
{
tag: dw_tag;
children: dw_entry list;