aboutsummaryrefslogtreecommitdiffstats
path: root/debug/DwarfTypes.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2014-11-11 18:42:51 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2014-11-11 18:42:51 +0100
commitac48235ec7485f659162d6220c8b4c7731505423 (patch)
tree59a828e7e21daa7682871b14173b8a177e92cab7 /debug/DwarfTypes.ml
parent977f81ff4962750f14970b8a32e30d90407572fe (diff)
downloadcompcert-ac48235ec7485f659162d6220c8b4c7731505423.tar.gz
compcert-ac48235ec7485f659162d6220c8b4c7731505423.zip
Added functions for printing of the abbreviations.
Diffstat (limited to 'debug/DwarfTypes.ml')
-rw-r--r--debug/DwarfTypes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/debug/DwarfTypes.ml b/debug/DwarfTypes.ml
index b2779e33..ecb346b9 100644
--- a/debug/DwarfTypes.ml
+++ b/debug/DwarfTypes.ml
@@ -36,7 +36,7 @@ type language =
| DW_LANG_C
| DW_LANG_C89
-type block = string (* Used as bitvector *)
+type block = string
type location_value =
| LocConst of constant