aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/coqlib.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index aac7f9a280..ab4a6a25cd 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -69,8 +69,8 @@ let check_required_library d =
let dir = make_dir d in
if Library.library_is_loaded dir then ()
else
- let in_current_dir = match Lib.current_prefix () with
- | MPfile dp, _ -> DirPath.equal dir dp
+ let in_current_dir = match Lib.current_mp () with
+ | MPfile dp -> DirPath.equal dir dp
| _ -> false
in
if not in_current_dir then