diff options
Diffstat (limited to 'library/nametab.ml')
| -rw-r--r-- | library/nametab.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index 7f148f0d3..a511a4e60 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -460,7 +460,7 @@ let basename_of_global ref = let path_of_syndef kn = Globrevtab.find (SynDef kn) !the_globrevtab -let dir_of_mp mp = +let dirpath_of_module mp = MPmap.find mp !the_modrevtab |