Pretty-printing preliminaire des modules, commandes

Print Module qid.
Print Module Type qid.
et affichage pendant
Print All.

Tout ca est preliminare, seuls les noms des composants sont affiches et
non pas les corps...


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2973 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 7 insertions, 5 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
diff --git a/kernel/names.mli b/kernel/names.mli
index b1bcc0b83b..d9b9ddc9cd 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -48,13 +48,14 @@ type mod_self_id
 (* The first argument is a file name - to prevent conflict between 
    different files *)
 val make_msid : dir_path -> string -> mod_self_id
-val string_of_msid : mod_self_id -> string
+val debug_string_of_msid : mod_self_id -> string
 
 (*s Unique names for bound modules *)
 type mod_bound_id
 
 val make_mbid : dir_path -> string -> mod_bound_id
-val string_of_mbid : mod_bound_id -> string
+val id_of_mbid : mod_bound_id -> identifier
+val debug_string_of_mbid : mod_bound_id -> string
 
 (*s Names of structure elements *)
 type label