diff options
| -rw-r--r-- | library/library.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/library.ml b/library/library.ml index ab92bb6769..fd9d93eb40 100644 --- a/library/library.ml +++ b/library/library.ml @@ -615,7 +615,7 @@ let import_module export (loc,qid) = if Lib.is_modtype () || Lib.is_module () || not export then add_anonymous_leaf (in_import (dir, export)) else - add_anonymous_leaf (in_require ([],[dir], Some export)) + add_anonymous_leaf (in_import (dir, export)) | mp -> Declaremods.import_module export mp with |