From f6d8fc17dc9474e4d043cf709d672d9259599354 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 22 Aug 2013 14:30:01 +0000
Subject: Nicer code concerning dirpaths and modpath around Lib

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16727 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/coqlib.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp')

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
-- 
cgit v1.2.3