diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index e94b73f180..3e34733f50 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -283,7 +283,10 @@ let _ = add "BeginModule" (function | [VARG_IDENTIFIER id] -> - fun () -> Lib.start_module (string_of_id id) + let s = string_of_id id in + let {relative_subdir = dir},_ = + System.find_file_in_path (Library.get_load_path ()) (s^".v") in + fun () -> Lib.start_module ((parse_loadpath dir)@[s]) | _ -> bad_vernac_args "BeginModule") let _ = |