aboutsummaryrefslogtreecommitdiffstats
path: root/lib
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2015-09-30 12:45:40 +0200
committerBernhard Schommer <bschommer@users.noreply.github.com>2015-09-30 12:45:40 +0200
commite443d76ad1ee0182353404317ab45c26227a59ea (patch)
tree1c110864431d8f6ba06c8746233397a3e221560e /lib
parentc212ab7a8adea516db72f17d818393629dbde1b3 (diff)
parentee76d81e0e7d8a76cd31bf0d01a532d248dca45a (diff)
downloadcompcert-e443d76ad1ee0182353404317ab45c26227a59ea.tar.gz
compcert-e443d76ad1ee0182353404317ab45c26227a59ea.zip
Merge pull request #56 from AbsInt/debug_locations
Debug locations
Diffstat (limited to 'lib')
-rw-r--r--lib/Camlcoq.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index 68c095f0..c50b3230 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -295,8 +295,7 @@ let intern_string s =
next_atom := Pos.succ !next_atom;
Hashtbl.add atom_of_string s a;
Hashtbl.add string_of_atom a s;
- a
-
+ a
let extern_atom a =
try
Hashtbl.find string_of_atom a