From 4f6b4c911f355b35c2b9a940cf78eb0cd21e4c12 Mon Sep 17 00:00:00 2001 From: filliatr Date: Mon, 23 Oct 2000 13:53:37 +0000 Subject: module_segment et module_filename git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@739 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/library.mli | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'library/library.mli') 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 -- cgit v1.2.3