From 53d23f52cd28c1373e784c278c8455cf9fa4eb67 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 12 Sep 2003 14:41:39 +0000
Subject: 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
---
 library/lib.ml | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index f24cf48922..179e51bf8e 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
-- 
cgit v1.2.3