diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index c30c6c0c1..18cef702c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -13,7 +13,6 @@ open Errors open Util open Flags open Names -open Entries open Nameops open Term open Pfedit @@ -26,13 +25,10 @@ open Command open Goptions open Libnames open Globnames -open Nametab open Vernacexpr open Decl_kinds open Constrexpr -open Pretyping open Redexpr -open Syntax_def open Lemmas open Declaremods open Misctypes |