diff options
Diffstat (limited to 'library/libnames.mli')
| -rw-r--r-- | library/libnames.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/library/libnames.mli b/library/libnames.mli index 915cdf3d2..04e552f4d 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -111,8 +111,3 @@ type global_dir_reference = | DirModule of object_prefix | DirClosedSection of dir_path (* this won't last long I hope! *) - -type strength = - | NotDeclare - | DischargeAt of dir_path * int - | NeverDischarge |