diff options
| author | soubiran | 2007-01-24 15:07:17 +0000 |
|---|---|---|
| committer | soubiran | 2007-01-24 15:07:17 +0000 |
| commit | dc57718e98289b5d71a0a942d6a063d441dc6a54 (patch) | |
| tree | 3e8136faef19ef7d1e8280177de78c56582d1f35 /kernel/names.ml | |
| parent | c155e42cdd1dd70b9e20243a6dc599ec653aef7a (diff) | |
modifications des messages d'erreurs renvoyés lors de la comparaison
de deux signatures de modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9531 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index d73af7fa1d..5dcd8a68f6 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -73,26 +73,33 @@ 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) + let debug_string_of_uid (i,s,p) = + "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">" let string_of_uid (i,s,p) = - "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">" + string_of_dirpath p ^"."^s module Umap = Map.Make(struct type t = uniq_ident let compare = Pervasives.compare end) +type label = string type mod_self_id = uniq_ident let make_msid = make_uid -let debug_string_of_msid = string_of_uid +let debug_string_of_msid = debug_string_of_uid +let string_of_msid = string_of_uid let id_of_msid (_,s,_) = s +let label_of_msid (_,s,_) = s type mod_bound_id = uniq_ident let make_mbid = make_uid -let debug_string_of_mbid = string_of_uid +let debug_string_of_mbid = debug_string_of_uid +let string_of_mbid = string_of_uid let id_of_mbid (_,s,_) = s +let label_of_mbid (_,s,_) = s + -type label = string let mk_label l = l let string_of_label l = l |