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
---
 pretyping/namegen.ml | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index a2fa81750c..1736bcff21 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -26,16 +26,14 @@ open Termops
 (**********************************************************************)
 (* Globality of identifiers *)
 
-let is_imported_modpath mp =
-  let current_mp,_ = Lib.current_prefix() in
-    match mp with
-      | MPfile dp ->
-	  let rec find_prefix = function
-	    |MPfile dp1 -> not (DirPath.equal dp1 dp)
-	    |MPdot(mp,_) -> find_prefix mp
-	    |MPbound(_) -> false
-	  in find_prefix current_mp
-      | p -> false
+let is_imported_modpath = function
+  | MPfile dp ->
+    let rec find_prefix = function
+      |MPfile dp1 -> not (DirPath.equal dp1 dp)
+      |MPdot(mp,_) -> find_prefix mp
+      |MPbound(_) -> false
+    in find_prefix (Lib.current_mp ())
+  | _ -> false
 
 let is_imported_ref = function
   | VarRef _ -> false
-- 
cgit v1.2.3