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/loadpath.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/loadpath.mli')
0 files changed, 0 insertions, 0 deletions