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
---
 printing/printer.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'printing')

diff --git a/printing/printer.ml b/printing/printer.ml
index cc9356cda7..05037a150f 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -144,12 +144,11 @@ let id_of_global env = function
     (Environ.lookup_mind kn env).mind_packets.(i).mind_consnames.(j-1)
   | VarRef v -> v
 
-let cons_dirpath id dp = DirPath.make (id :: DirPath.repr dp)
-
 let rec dirpath_of_mp = function
   | MPfile sl -> sl
   | MPbound uid -> DirPath.make [MBId.to_id uid]
-  | MPdot (mp,l) -> cons_dirpath (Label.to_id l) (dirpath_of_mp mp)
+  | MPdot (mp,l) ->
+    Libnames.add_dirpath_suffix (dirpath_of_mp mp) (Label.to_id l)
 
 let dirpath_of_global = function
   | ConstRef kn -> dirpath_of_mp (Constant.modpath kn)
-- 
cgit v1.2.3