From 8d4ca0e78b9ba99b6ff1f9e00e3ea9a4e70e3fd7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 23 Dec 2005 10:06:29 +0000
Subject: Correction pr_module pour traducteur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7708 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 translate/ppvernacnew.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index bfe948c53f..154d23c38d 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -60,9 +60,12 @@ let pr_module r =
         Ident (loc,id_of_string s)
     | Qualid (loc,qid) ->
         Qualid (loc,make_qualid (fst (repr_qualid qid)) (id_of_string s)) in
-  let (_,dir,_) =
+  let dir =
     try
-      Library.locate_qualified_library (snd (qualid_of_reference r))
+      Nametab.full_name_module (snd (qualid_of_reference r))
+    with _ -> 
+    try
+      pi2 (Library.locate_qualified_library (snd (qualid_of_reference r)))
     with _ -> 
       errorlabstrm "" (str"Translator cannot find " ++ Libnames.pr_reference r)
   in
-- 
cgit v1.2.3