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