From 6dbe0f97c7f23de89b90e232bc812b77dde86cac Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 14 Dec 2012 11:27:47 +0000
Subject: Moving hcons_string to String namespace.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16069 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/names.ml  | 10 ++++------
 kernel/names.mli |  1 -
 2 files changed, 4 insertions(+), 7 deletions(-)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index c4e632a3a2..1917f8f40a 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -22,8 +22,6 @@ open Pp
 open Errors
 open Util
 
-let hcons_string = Hashcons.simple_hcons Hashcons.Hstring.generate ()
-
 (** {6 Identifiers } *)
 
 type identifier = string
@@ -38,7 +36,7 @@ let check_ident x =
 let id_of_string s =
   let () = check_ident_soft s in
   let s = String.copy s in
-  hcons_string s
+  String.hcons s
 
 let string_of_id id = String.copy id
 
@@ -504,13 +502,13 @@ module Hconstruct = Hashcons.Make(
     let hash = Hashtbl.hash
   end)
 
-let hcons_ident = hcons_string
+let hcons_ident = String.hcons
 let hcons_name = Hashcons.simple_hcons Hname.generate hcons_ident
 let hcons_dirpath = Hashcons.simple_hcons Hdir.generate hcons_ident
 let hcons_uid = Hashcons.simple_hcons Huniqid.generate (hcons_ident,hcons_dirpath)
 let hcons_mp =
-  Hashcons.simple_hcons Hmod.generate (hcons_dirpath,hcons_uid,hcons_string)
-let hcons_kn = Hashcons.simple_hcons Hkn.generate (hcons_mp,hcons_dirpath,hcons_string)
+  Hashcons.simple_hcons Hmod.generate (hcons_dirpath,hcons_uid,String.hcons)
+let hcons_kn = Hashcons.simple_hcons Hkn.generate (hcons_mp,hcons_dirpath,String.hcons)
 let hcons_con = Hashcons.simple_hcons Hcn.generate hcons_kn
 let hcons_mind = Hashcons.simple_hcons Hcn.generate hcons_kn
 let hcons_ind = Hashcons.simple_hcons Hind.generate hcons_mind
diff --git a/kernel/names.mli b/kernel/names.mli
index 3eb0703803..0f37c80550 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -220,7 +220,6 @@ val eq_egr : evaluable_global_reference ->  evaluable_global_reference
 
 (** {6 Hash-consing } *)
 
-val hcons_string : string -> string
 val hcons_ident : identifier -> identifier
 val hcons_name : name -> name
 val hcons_dirpath : dir_path -> dir_path
-- 
cgit v1.2.3