module_segment et module_filename

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

1 files changed, 9 insertions, 1 deletions

diff --git a/library/library.mli b/library/library.mli
index 0eb47bd3a..474669452 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -1,7 +1,7 @@
 
 (* $Id$ *)
 
-(* This module is the heart of the library. It provides low level functions to
+(*s This module is the heart of the library. It provides low level functions to
    load, open and save modules. Modules are saved onto the disk with checksums
    (obtained with the [Digest] module), which are checked at loading time to
    prevent inconsistencies between files written at various dates. It also
@@ -32,6 +32,14 @@ val require_module : bool option -> string -> string option -> bool -> unit
 
 val save_module_to : string -> string -> unit
 
+(*s [module_segment m] returns the segment of the loaded module
+    [m]; if not given, the segment of the current module is returned
+    (which is then the same as [Lib.contents_after None]). 
+    [module_filename] returns the full filename of a loaded module. *)
+
+val module_segment : string option -> Lib.library_segment
+val module_filename : string -> string
+
 (*s Global load path *)
 val get_load_path : unit -> string list
 val add_path : string -> unit