module Library

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

1 files changed, 28 insertions, 0 deletions

diff --git a/library/library.mli b/library/library.mli
new file mode 100644
index 000000000..2c54aec2e
--- /dev/null
+++ b/library/library.mli
@@ -0,0 +1,28 @@
+
+(* $Id$ *)
+
+(* 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
+   provides a high level function [require] which corresponds to the 
+   vernacular command [Require]. *)
+
+val load_module : string -> string option -> unit
+val open_module : string -> unit
+
+val module_is_loaded : string -> bool
+val module_is_opened : string -> bool
+
+(*s Require. The command [require_module spec m file export] loads and opens
+  a module [m]. [file] specifies the filename, if not [None]. [spec]
+  specifies to look for a specification ([true]) or for an implementation
+  ([false]), if not [None]. And [export] specifies if the module must be 
+  exported. *)
+
+val require_module : bool option -> string -> string option -> bool -> unit
+
+(*s [save_module_to s f] saves the current environment as a module [s]
+  in the file [f]. *)
+
+val save_module_to : string -> string -> unit