diff options
Diffstat (limited to 'library/libnames.ml')
| -rw-r--r-- | library/libnames.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/library/libnames.ml b/library/libnames.ml index d5e9c8dc7..19e7d2833 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -205,8 +205,3 @@ type global_dir_reference = let kn' = subst_kernel_name subst kn in if kn==kn' then ref else ModTypeRef kn' *) - -type strength = - | NotDeclare - | DischargeAt of dir_path * int - | NeverDischarge |