From c0e397fca7fd2f150c68ab043fd8fdd15db5bcdf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 30 Mar 2010 15:09:10 +0000
Subject: Fixed small bugs introduced in commit 12890 (bug #2286, that comes
 from a incorrect computation of logical names + bug in rendering of
 name-based notations, aka abbreviations or syntactic definitions).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12893 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tools/coqdoc/main.ml | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'tools/coqdoc/main.ml')

diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index fb9b64b4fb..b52c28ff29 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -134,13 +134,12 @@ let add_path dir name =
   paths := (p,name) :: !paths
 
 (* turn A/B/C into A.B.C *)
-let rec name_of_path p name fname suffix =
-  let dir = Filename.dirname fname in
-  if dir = fname then raise Not_found
+let rec name_of_path p name dirname suffix =
+  if p = dirname then String.concat "." (name::suffix)
   else
-    let base = Filename.basename fname in
-    if p = dir then String.concat "." (name::base::suffix)
-    else name_of_path p name dir (base::suffix)
+    let subdir = Filename.dirname dirname in
+    if subdir = dirname then raise Not_found
+    else name_of_path p name subdir (Filename.basename dirname::suffix)
 
 let coq_module filename =
   let bfname = Filename.chop_extension filename in
-- 
cgit v1.2.3