1 files changed, 18 insertions, 0 deletions
diff --git a/library/lib.ml b/library/lib.ml
index ca054c8d6c..0b383b34d8 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