Module Nametab.GlobDirRef
to this type are mapped DirPath.t's in the nametab
type t=|DirOpenModule of Names.ModPath.t|DirOpenModtype of Names.ModPath.t|DirOpenSection of Names.DirPath.t
Nametab.GlobDirRefto this type are mapped DirPath.t's in the nametab
type t = | DirOpenModule of Names.ModPath.t |
| DirOpenModtype of Names.ModPath.t |
| DirOpenSection of Names.DirPath.t |