diff options
Diffstat (limited to 'library/libnames.mli')
| -rw-r--r-- | library/libnames.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/library/libnames.mli b/library/libnames.mli index 9dad26129..81e5bc5b1 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -125,8 +125,6 @@ type global_dir_reference = | DirOpenModtype of object_prefix | DirOpenSection of object_prefix | DirModule of object_prefix - | DirClosedSection of DirPath.t - (** this won't last long I hope! *) val eq_global_dir_reference : global_dir_reference -> global_dir_reference -> bool |