Déplacement de Declare juste à la fin de interp pour pouvoir accéder à interp

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

1 files changed, 16 insertions, 0 deletions

diff --git a/library/lib.ml b/library/lib.ml
index f24cf4892..179e51bf8 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -525,3 +525,19 @@ let reset_initial () =
 	end
 
 
+(* Misc *)
+
+let library_part ref =
+  let sp = Nametab.sp_of_global ref in
+  let dir,_ = repr_path sp in
+  match ref with
+  | VarRef id -> 
+      anomaly "TODO";
+      extract_dirpath_prefix (sections_depth ()) (cwd ())
+  | _ ->
+      if is_dirpath_prefix_of dir (cwd ()) then
+        (* Not yet (fully) discharged *)
+        extract_dirpath_prefix (sections_depth ()) (cwd ())
+      else
+	(* Theorem/Lemma outside its outer section of definition *)
+	dir