aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacentries.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vernacentries.ml')
-rw-r--r--toplevel/vernacentries.ml4
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