aboutsummaryrefslogtreecommitdiff
path: root/kernel/names.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/names.ml')
-rw-r--r--kernel/names.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index c85389434f..d926779430 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -389,7 +389,7 @@ module Hcn = Hashcons.Make(
let hash x = Hashtbl.hash (fst x)
end)
-let hcons_names () =
+let hcons_names =
let hstring = Hashcons.simple_hcons Hashcons.Hstring.f () in
let hident = hstring in
let hname = Hashcons.simple_hcons Hname.f hident in