From 3386a50c15ddc367cd247f288ff84f288a0c42af Mon Sep 17 00:00:00 2001 From: filliatr Date: Sat, 18 Sep 1999 16:13:36 +0000 Subject: module Library git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@74 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/library.mli | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 library/library.mli (limited to 'library/library.mli') 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 -- cgit v1.2.3