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/cpretty.mll |  2 +-
 tools/coqdoc/main.ml     | 11 +++++------
 2 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 97d581048a..1834a7d336 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -1079,7 +1079,7 @@ and start_notation_string = parse
         notation_string lexbuf;
 	body lexbuf }
   | _ (* an abbreviation *)
-      { body lexbuf }
+      { backtrack lexbuf; body lexbuf }
 
 and notation_string = parse
   | "\"\""
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