aboutsummaryrefslogtreecommitdiffstats
path: root/debug/DwarfUtil.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2014-11-17 13:33:17 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2014-11-17 13:33:17 +0100
commit19e69e76b4608ab86819deb301409824400425a1 (patch)
tree73f8f90c0ea27d3fba68bfc89a42b93f6fe0363e /debug/DwarfUtil.ml
parent5725e8d4ffcc9bde14b0c46fcaba83a9d84c7ddb (diff)
downloadcompcert-19e69e76b4608ab86819deb301409824400425a1.tar.gz
compcert-19e69e76b4608ab86819deb301409824400425a1.zip
Removed compile error and added dummy function for the printing of entries.
Diffstat (limited to 'debug/DwarfUtil.ml')
-rw-r--r--debug/DwarfUtil.ml5
1 files changed, 0 insertions, 5 deletions
diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml
index 5bdba147..79516e65 100644
--- a/debug/DwarfUtil.ml
+++ b/debug/DwarfUtil.ml
@@ -44,11 +44,6 @@ let add_children entry child =
{entry with children = child::entry.children;}
-(* Iter over the tree in prefix order *)
-let rec entry_iter f entry =
- f entry.tag;
- List.iter (entry_iter f) entry.children
-
let list_iter_with_next f list =
let rec aux = (function
| [] -> ()