diff options
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 0209d1c33d..b67fd32ad5 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -71,7 +71,7 @@ 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,s,dir) +let make_uid dir s = incr u_number;(!u_number,String.copy s,dir) let string_of_uid (i,s,p) = "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">" @@ -83,11 +83,12 @@ module Umap = Map.Make(struct type mod_self_id = uniq_ident let make_msid = make_uid -let string_of_msid = string_of_uid +let debug_string_of_msid = string_of_uid type mod_bound_id = uniq_ident let make_mbid = make_uid -let string_of_mbid = string_of_uid +let debug_string_of_mbid = string_of_uid +let id_of_mbid (_,s,_) = s type label = string let mk_label l = l |