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.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'library/lib.mli')

diff --git a/library/lib.mli b/library/lib.mli
index 2f51d441d9..e16f44af81 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -117,6 +117,9 @@ val end_compilation : dir_path -> object_prefix * library_segment
    compiling library (or [default_library]) *)
 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
+
 (*s Sections *)
 
 val open_section : identifier -> object_prefix
-- 
cgit v1.2.3