From 262ad3c3ce24463094110aa011471213ac0b61c7 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 18 Aug 2016 18:47:55 +0200 Subject: Fix incorrect glob data for module symbols (bug #2336). The logic was backward: if the path of a symbol was a prefix of the current path, then the current path (without sections) was used. But what we want is that, if the current path (without sections) is a prefix of the path of a symbol, then the former should be used. This fixes about 1,600 broken links in the documentation of the standard library. --- interp/dumpglob.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'interp/dumpglob.ml') diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 85212b7ab..d70d30d9e 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -127,9 +127,10 @@ let type_of_global_ref gr = | Globnames.ConstructRef _ -> "constr" let remove_sections dir = - if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then + let cwd = Lib.cwd_except_section () in + if Libnames.is_dirpath_prefix_of cwd dir then (* Not yet (fully) discharged *) - Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) + cwd else (* Theorem/Lemma outside its outer section of definition *) dir -- cgit v1.2.3