diff options
-rw-r--r-- | kernel/names.ml | 10 | ||||
-rw-r--r-- | kernel/names.mli | 4 | ||||
-rw-r--r-- | library/declaremods.ml | 2 | ||||
-rw-r--r-- | library/lib.ml | 2 | ||||
-rw-r--r-- | parsing/ppvernac.ml | 2 |
5 files changed, 10 insertions, 10 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index c65e624c2..c85389434 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -72,8 +72,8 @@ let string_of_dirpath = function let u_number = ref 0 -type uniq_ident = int * string * dir_path -let make_uid dir s = incr u_number;(!u_number,String.copy s,dir) +type uniq_ident = int * identifier * dir_path +let make_uid dir s = incr u_number;(!u_number,s,dir) let debug_string_of_uid (i,s,p) = "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">" let string_of_uid (i,s,p) = @@ -347,8 +347,8 @@ module Hdir = Hashcons.Make( module Huniqid = Hashcons.Make( struct type t = uniq_ident - type u = (string -> string) * (dir_path -> dir_path) - let hash_sub (hstr,hdir) (n,s,dir) = (n,hstr s,hdir dir) + type u = (identifier -> identifier) * (dir_path -> dir_path) + let hash_sub (hid,hdir) (n,s,dir) = (n,hid s,hdir dir) let equal (n1,s1,dir1) (n2,s2,dir2) = n1 = n2 && s1 == s2 && dir1 == dir2 let hash = Hashtbl.hash end) @@ -394,7 +394,7 @@ let hcons_names () = let hident = hstring in let hname = Hashcons.simple_hcons Hname.f hident in let hdir = Hashcons.simple_hcons Hdir.f hident in - let huniqid = Hashcons.simple_hcons Huniqid.f (hstring,hdir) in + let huniqid = Hashcons.simple_hcons Huniqid.f (hident,hdir) in let hmod = Hashcons.simple_hcons Hmod.f (hdir,huniqid,hstring) in let hmind = Hashcons.simple_hcons Hcn.f (hmod,hdir,hstring) in let hcn = Hashcons.simple_hcons Hcn.f (hmod,hdir,hstring) in diff --git a/kernel/names.mli b/kernel/names.mli index 62d2040c2..8a2e892ef 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -62,8 +62,8 @@ type mod_bound_id (** The first argument is a file name - to prevent conflict between different files *) -val make_mbid : dir_path -> string -> mod_bound_id -val repr_mbid : mod_bound_id -> int * string * dir_path +val make_mbid : dir_path -> identifier -> mod_bound_id +val repr_mbid : mod_bound_id -> int * identifier * dir_path val id_of_mbid : mod_bound_id -> identifier val label_of_mbid : mod_bound_id -> label val debug_string_of_mbid : mod_bound_id -> string diff --git a/library/declaremods.ml b/library/declaremods.ml index 8753624a9..d4712762a 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -545,7 +545,7 @@ let process_module_seb_binding mbid seb = let intern_args interp_modtype (idl,(arg,ann)) = let inl = inline_annot ann in let lib_dir = Lib.library_dp() in - let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in + let mbids = List.map (fun (_,id) -> make_mbid lib_dir id) idl in let mty = interp_modtype (Global.env()) arg in let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in let (mbi,mp_from,objs) = get_modtype_substobjs (Global.env()) diff --git a/library/lib.ml b/library/lib.ml index cfaea3b66..23d334a5d 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -728,7 +728,7 @@ let rec split_mp mp = | Names.MPdot (prfx, lbl) -> let mprec, dprec = split_mp prfx in mprec, Names.make_dirpath (Names.id_of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec)) - | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in library_dp(), Names.make_dirpath [Names.id_of_string id] + | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in library_dp(), Names.make_dirpath [id] let split_modpath mp = let rec aux = function diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index bb20dc7fc..b1ba16b5c 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -260,7 +260,7 @@ let pr_module_vardecls pr_c (export,idl,(mty,inl)) = let lib_dir = Lib.library_dp() in List.iter (fun (_,id) -> Declaremods.process_module_bindings [id] - [make_mbid lib_dir (string_of_id id), + [make_mbid lib_dir id, (Modintern.interp_modtype (Global.env()) mty, inl)]) idl; (* Builds the stream *) spc() ++ |