22 files changed, 0 insertions, 54 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 846fb5b934..37e627a6d4 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -7,16 +7,7 @@
 (************************************************************************)
 
 open Loc
-open Pp
-open Names
-open Term
-open Libnames
-open Globnames
-open Glob_term
-open Genredexpr
 open Tacexpr
-open Pattern
-open Constrexpr
 open Term
 open Misctypes
 open Genarg
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index c49b61ce78..5faef378a6 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -14,7 +14,6 @@ open Names
 open Term
 open Libnames
 open Globnames
-open Glob_term
 open Genredexpr
 open Pattern
 open Constrexpr
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 687f5cb9e5..25194acc93 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -7,12 +7,9 @@
 (************************************************************************)
 
 open Loc
-open Pp
 open Names
 open Libnames
 open Misctypes
-open Term
-open Mod_subst
 open Constrexpr
 
 (** Constrexpr_ops: utilities on [constr_expr] *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index a3410544ef..6a893bde64 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -26,7 +26,6 @@ open Glob_ops
 open Pattern
 open Nametab
 open Notation
-open Reserve
 open Detyping
 open Misctypes
 open Decl_kinds
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index a98182fb87..e1acb45021 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
 open Term
 open Context
@@ -14,7 +13,6 @@ open Termops
 open Environ
 open Libnames
 open Globnames
-open Nametab
 open Glob_term
 open Pattern
 open Constrexpr
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 5b5775d1a3..a1faf95e21 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -9,7 +9,6 @@
 open Pp
 open Errors
 open Util
-open Flags
 open Names
 open Nameops
 open Namegen
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 90c3779fc6..a0bcdc4f4e 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -17,7 +17,6 @@ open Glob_term
 open Pattern
 open Constrexpr
 open Notation_term
-open Termops
 open Pretyping
 open Misctypes
 open Decl_kinds
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 9e0cfadae9..9b0f8deb9c 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -9,9 +9,7 @@
 open Names
 open Libnames
 open Globnames
-open Nametab
 open Term
-open Pattern
 open Util
 
 (** This module collects the global references, constructions and
diff --git a/interp/genintern.ml b/interp/genintern.ml
index bc41c834a8..a8f82d9984 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
-open Util
 open Names
 open Mod_subst
 open Genarg
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 4d4fe91173..2d55a6b63b 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -14,7 +14,6 @@ open Util
 open Glob_term
 open Constrexpr
 open Libnames
-open Globnames
 open Typeclasses
 open Typeclasses_errors
 open Pp
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index df29d05926..50c2cfee02 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -8,19 +8,10 @@
 
 open Loc
 open Names
-open Decl_kinds
-open Term
-open Context
-open Evd
-open Environ
-open Nametab
-open Mod_subst
 open Glob_term
 open Constrexpr
-open Pp
 open Libnames
 open Globnames
-open Typeclasses
 
 val declare_generalizable : Vernacexpr.locality_flag -> (Id.t located) list option -> unit
 
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 8f8e2df93e..81d0a0f644 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Declarations
-open Entries
 open Libnames
 open Constrexpr
 open Constrintern
diff --git a/interp/modintern.mli b/interp/modintern.mli
index b6128918c1..a3998cf833 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -6,13 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
-open Declarations
 open Environ
 open Entries
-open Pp
-open Libnames
-open Names
 open Constrexpr
 open Misctypes
 
diff --git a/interp/notation.mli b/interp/notation.mli
index a4ca3ffaab..95e176064c 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -9,7 +9,6 @@
 open Pp
 open Bigint
 open Names
-open Nametab
 open Libnames
 open Globnames
 open Constrexpr
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 4f84af5fe3..fd442cdb4e 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Notation_term
-open Misctypes
 open Glob_term
 
 (** Utilities about [notation_constr] *)
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index cae644ab5b..d1bcb0cf18 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Names
 
 (** {6 Pretty-print. } *)
 
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 6674a8323a..c104d0d155 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -123,8 +123,6 @@ let revert_reserved_type t =
 
 let _ = Namegen.set_reserved_typed_name revert_reserved_type
 
-open Glob_term
-
 let default_env () = {
   ninterp_var_type = Id.Map.empty;
   ninterp_rec_vars = Id.Map.empty;
diff --git a/interp/reserve.mli b/interp/reserve.mli
index 8ae55d0961..81590bd1c6 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -7,9 +7,7 @@
 (************************************************************************)
 
 open Loc
-open Pp
 open Names
-open Glob_term
 open Notation_term
 
 val declare_reserved_type : Id.t located list -> notation_constr -> unit
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 5f772c5915..86aa69681d 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Loc
-open Pp
 open Names
 open Libnames
 open Globnames
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 6f2ff6ec48..0f4e8a5885 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Genarg
 
 let wit_unit : unit uniform_genarg_type =
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index f3c4a61e62..065cbe3ec4 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -8,9 +8,6 @@
 
 open Names
 open Notation_term
-open Glob_term
-open Nametab
-open Libnames
 
 (** Syntactic definitions. *)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index f042de00ff..c85d516675 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -8,11 +8,7 @@
 
 open Loc
 open Names
-open Libnames
-open Misctypes
-open Decl_kinds
 open Constrexpr
-open Notation_term
 
 (** Topconstr *)