diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-01 18:09:44 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-04 19:58:59 +0100 |
| commit | 9347618755eed17d683f590f8bd9c47aacfcfa17 (patch) | |
| tree | b8fa7da833a326d06e742b636177a63d0e44d143 /library/library.mli | |
| parent | 626aaf5652589ae69e95756859ced47e81b25b17 (diff) | |
Optimized Import/Export the same way as Require Import/Export was
optimized. Now "Import Arith ZArith" imports only once the libraries
reexported by both Arith and ZArith. (No side effect can be inserted
here, so that this looks compatible).
Diffstat (limited to 'library/library.mli')
| -rw-r--r-- | library/library.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/library.mli b/library/library.mli index 13d83a5c0..77d78207d 100644 --- a/library/library.mli +++ b/library/library.mli @@ -37,7 +37,7 @@ type seg_proofs = Term.constr Future.computation array (** Open a module (or a library); if the boolean is true then it's also an export otherwise just a simple import *) -val import_module : bool -> qualid located -> unit +val import_module : bool -> qualid located list -> unit (** {6 Start the compilation of a library } *) val start_library : string -> DirPath.t * string |