5 files changed, 30 insertions, 3 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 9e6cbaf44..5f358e694 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -39,8 +39,8 @@ let interning_grammar = ref false
 let for_grammar f x =
   interning_grammar := true;
   let a = f x in
-  interning_grammar := false;
-  a
+    interning_grammar := false;
+    a
 
 let variables_bind = ref false
 
@@ -140,7 +140,7 @@ let coqdoc_unfreeze (lt,tn,lp) =
 
 let add_glob loc ref = 
   let sp = Nametab.sp_of_global ref in
-  let lib_dp = Lib.library_dp() in
+  let lib_dp = Lib.library_part ref in
   let mod_dp,id = repr_path sp in
   let mod_dp_trunc =  drop_dirpath_prefix lib_dp mod_dp in
   let filepath = string_of_dirpath lib_dp in
diff --git a/kernel/names.ml b/kernel/names.ml
index 7b83e18c3..d73af7fa1 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -198,6 +198,10 @@ let con_label = label
 let pr_con = pr_kn
 let con_modpath = modpath
 
+let mind_modpath = modpath
+let ind_modpath ind = mind_modpath (fst ind)
+let constr_modpath c = ind_modpath (fst c)
+
 let ith_mutual_inductive (kn,_) i = (kn,i)
 let ith_constructor_of_inductive ind i = (ind,i)
 let inductive_of_constructor (ind,i) = ind
diff --git a/kernel/names.mli b/kernel/names.mli
index 0e65b65b4..4c51269d0 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -134,6 +134,10 @@ val con_label : constant -> label
 val con_modpath : constant -> module_path
 val pr_con : constant -> Pp.std_ppcmds
 
+val mind_modpath : mutual_inductive -> module_path
+val ind_modpath : inductive -> module_path
+val constr_modpath : constructor -> module_path
+
 val ith_mutual_inductive : inductive -> int -> inductive
 val ith_constructor_of_inductive : inductive -> int -> constructor
 val inductive_of_constructor : constructor -> inductive
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
diff --git a/library/lib.mli b/library/lib.mli
index 6552cda6a..52e6b7bd7 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -122,6 +122,7 @@ val end_compilation : dir_path -> object_prefix * library_segment
 val library_dp : unit -> dir_path
 
 (* Extract the library part of a name even if in a section *)
+val library_part :  global_reference -> dir_path
 val remove_section_part : global_reference -> dir_path
 
 (*s Sections *)