From c25ff7718d77e4aba0827c4d45a507ed49db72e0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 21 Oct 2014 22:09:35 +0200
Subject: Fixing what really looks like a bug in the initial implementation of
 coqdoc links for modules (#3756).

---
 interp/dumpglob.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 87c8cb04d9..a9b8ccb426 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -153,7 +153,6 @@ let dump_reference loc modpath ident ty =
 let dump_modref loc mp ty =
   let (dp, l) = Lib.split_modpath mp in
   let filepath = Names.DirPath.to_string dp in
-  let l = if List.is_empty l then l else List.drop_last l in
   let modpath = Names.DirPath.to_string (Names.DirPath.make l) in
   let ident = "<>" in
   dump_ref loc filepath modpath ident ty
-- 
cgit v1.2.3