Affichage des dir_path vide

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

1 files changed, 5 insertions, 2 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index a6463a7bd..b79a52608 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -249,7 +249,9 @@ let dirpath_of_string s =
   with
     | Invalid_argument _ -> invalid_arg "dirpath_of_string"
 
-let string_of_dirpath sl = String.concat "." (List.map string_of_id sl)
+let string_of_dirpath = function
+  | [] -> "<empty>"
+  | sl -> String.concat "." (List.map string_of_id sl)
 
 let pr_dirpath sl = [< 'sTR (string_of_dirpath sl) >]
 
@@ -270,7 +272,8 @@ let dirpath sp = sp.dirpath
 (* parsing and printing of section paths *)
 let string_of_path sp =
   let (sl,id,k) = repr_path sp in
-  (string_of_dirpath sl) ^ "." ^ (string_of_id id)
+  if sl = [] then string_of_id id
+  else (string_of_dirpath sl) ^ "." ^ (string_of_id id)
 
 let path_of_string s =
   try