diff options
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/library/declare.ml b/library/declare.ml index 3a8f32408..4fae644c2 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -26,7 +26,6 @@ open Libobject open Lib open Impargs open Nametab -open Library open Safe_typing open Decl_kinds |