diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-21 22:09:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-22 11:04:30 +0200 |
| commit | c25ff7718d77e4aba0827c4d45a507ed49db72e0 (patch) | |
| tree | 4c4f05548fa696fe97343506802782049ee81bac /interp | |
| parent | 04a7118e26ed3bb3b98ed68a394f7eaed2a0cb81 (diff) | |
Fixing what really looks like a bug in the initial implementation of
coqdoc links for modules (#3756).
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/dumpglob.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 87c8cb04d..a9b8ccb42 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 |