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.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 |