aboutsummaryrefslogtreecommitdiffstats
path: root/debug/DebugInit.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-03-18 13:17:09 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2016-03-18 13:17:09 +0100
commitd9c0c49cf32be6aa17918654c05bee45f29fb737 (patch)
treed9f0f034c48553840126414ee9daca4d018ece16 /debug/DebugInit.ml
parent1e08d4adb241e076a96f9525fdb8359cf8845527 (diff)
downloadcompcert-kvx-d9c0c49cf32be6aa17918654c05bee45f29fb737.tar.gz
compcert-kvx-d9c0c49cf32be6aa17918654c05bee45f29fb737.zip
Added an interface file for DebugInformation.
The interface hides the implementation details, like the huge number of Hashtbls from the rest of the implementatio. Bug 18394
Diffstat (limited to 'debug/DebugInit.ml')
-rw-r--r--debug/DebugInit.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml
index 24712b27..462ca2d3 100644
--- a/debug/DebugInit.ml
+++ b/debug/DebugInit.ml
@@ -22,7 +22,7 @@ let default_debug =
insert_global_declaration = DebugInformation.insert_global_declaration;
add_fun_addr = (fun _ _ _ -> ());
generate_debug_info = (fun _ _ -> None);
- all_files_iter = (fun f -> DebugInformation.StringSet.iter f !DebugInformation.all_files);
+ all_files_iter = DebugInformation.all_files_iter;
insert_local_declaration = DebugInformation.insert_local_declaration;
atom_local_variable = DebugInformation.atom_local_variable;
enter_scope = DebugInformation.enter_scope;