diff options
Diffstat (limited to 'library/library.ml')
| -rw-r--r-- | library/library.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/library/library.ml b/library/library.ml index b9f1b109a3..cd99b603e2 100644 --- a/library/library.ml +++ b/library/library.ml @@ -159,7 +159,8 @@ let rec load_module_from s f = List.iter (load_mandatory_module s) m.module_deps; Global.import m.module_compiled_env; load_objects m.module_declarations; - let sp = Names.make_path [] (id_of_string s) CCI in + let dir = parse_loadpath lpe.relative_subdir in + let sp = Names.make_path dir (id_of_string s) CCI in Nametab.push_module sp m.module_nametab; modules_table := Stringmap.add s m !modules_table; m |