Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_sp

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

2 files changed, 8 insertions, 8 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 76f17525d..c8eb17ca9 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -55,7 +55,7 @@ let id_of_string s =
 let atompart_of_id id = id.atom
 let index_of_id id = snd (repr_ident id)
 
-let print_id id =
+let pr_id id =
   match repr_ident id with
     | ("",None)   -> [< 'sTR"[]" >]
     | ("",Some n) -> [< 'sTR"[" ; 'iNT n ; 'sTR"]" >]
@@ -134,7 +134,7 @@ let make_qualid p s = (p,s)
 let repr_qualid q = q
 
 let string_of_qualid (l,s) = String.concat "." (l@[s])
-let print_qualid (l,s) = prlist_with_sep (fun () -> pr_str ".") pr_str (l@[s])
+let pr_qualid (l,s) = prlist_with_sep (fun () -> pr_str ".") pr_str (l@[s])
 
 (*s Section paths *)
 
@@ -158,8 +158,8 @@ let string_of_dirpath sl = String.concat "#" (""::sl)
 let string_of_path sp =
   let (sl,id,k) = repr_path sp in
   String.concat ""
-    ((List.flatten (List.map (fun s -> ["#";s]) sl))
-     @ [ "#"; string_of_id id; "."; string_of_kind k ])
+    ("#"::(List.flatten (List.map (fun s -> [s;"."]) sl))
+     @ [ string_of_id id ])
     
 let path_of_string s =
   try
@@ -168,7 +168,7 @@ let path_of_string s =
   with
     | Invalid_argument _ -> invalid_arg "path_of_string"
 
-let print_sp sp = [< 'sTR (string_of_path sp) >]
+let pr_sp sp = [< 'sTR (string_of_path sp) >]
 
 let sp_of_wd = function
   | [] -> invalid_arg "Names.sp_of_wd"
diff --git a/kernel/names.mli b/kernel/names.mli
index 3a380a42d..070e7917f 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -23,7 +23,7 @@ val index_of_id : identifier -> int option
 (* Parsing and printing of identifiers *)
 val string_of_id : identifier -> string
 val id_of_string : string -> identifier
-val print_id : identifier -> std_ppcmds
+val pr_id : identifier -> std_ppcmds
 
 (* Identifiers sets and maps *)
 module Idset : Set.S with type elt = identifier
@@ -58,7 +58,7 @@ val make_qualid : string list -> string -> qualid
 val repr_qualid : qualid -> string list * string
 
 val string_of_qualid : qualid -> string
-val print_qualid : qualid -> std_ppcmds
+val pr_qualid : qualid -> std_ppcmds
 
 (*s Section paths *)
 type section_path
@@ -78,7 +78,7 @@ val wd_of_sp : section_path -> string list
 (* Parsing and printing of section path as ["#module#id#kind"] *)
 val path_of_string : string -> section_path
 val string_of_path : section_path -> string
-val print_sp : section_path -> std_ppcmds
+val pr_sp : section_path -> std_ppcmds
 
 (*i
 val string_of_path_mind : section_path -> identifier -> string