Modification de add_glob (support des modules dans Coqdoc)

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

1 files changed, 18 insertions, 0 deletions

diff --git a/library/lib.ml b/library/lib.ml
index ca054c8d6..0b383b34d 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -624,6 +624,24 @@ let reset_initial () =
 
 (* Misc *)
 
+let mp_of_global ref = 
+  match ref with
+    | VarRef id -> fst (current_prefix ())
+    | ConstRef cst -> con_modpath cst
+    | IndRef ind -> ind_modpath ind
+    | ConstructRef constr -> constr_modpath constr
+
+let rec dp_of_mp modp =
+  match modp with
+    | MPfile dp -> dp
+    | MPbound _ | MPself _ -> library_dp ()
+    | MPdot (mp,_) -> dp_of_mp mp
+
+let library_part ref =
+  match ref with 
+    | VarRef id -> library_dp ()
+    | _ -> dp_of_mp (mp_of_global ref)
+
 let remove_section_part ref =
   let sp = Nametab.sp_of_global ref in
   let dir,_ = repr_path sp in