From f6d8fc17dc9474e4d043cf709d672d9259599354 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
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
---
 plugins/xml/xmlcommand.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'plugins/xml')

diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 6145548b2..d065ba61a 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -380,10 +380,7 @@ let print internal glob_ref kind xml_library_root =
    match glob_ref with
       Gn.VarRef id ->
        (* this kn is fake since it is not provided by Coq *)
-       let kn =
-        let (mod_path,dir_path) = Lib.current_prefix () in
-        N.make_kn mod_path dir_path (N.Label.of_id id)
-       in
+       let kn = Lib.make_kn id in
        let (_,body,typ) = G.lookup_named id in
         Cic2acic.Variable kn,mk_variable_obj id body typ
     | Gn.ConstRef kn ->
-- 
cgit v1.2.3