Remove many superfluous 'open' indicated by ocamlc -w +33

 With ocaml 4.01, the 'unused open' warning also checks the mli :-)

 Beware: some open are reported as useless when compiling with camlp5,
 but are necessary for compatibility with camlp4. These open are now
 marked with a comment.

22 files changed, 0 insertions, 54 deletions

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 846fb5b93..37e627a6d 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 c49b61ce7..5faef378a 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 687f5cb9e..25194acc9 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 a3410544e..6a893bde6 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 a98182fb8..e1acb4502 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 5b5775d1a..a1faf95e2 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 90c3779fc..a0bcdc4f4 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 9e0cfadae..9b0f8deb9 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 bc41c834a..a8f82d998 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 4d4fe9117..2d55a6b63 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 df29d0592..50c2cfee0 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 8f8e2df93..81d0a0f64 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 b6128918c..a3998cf83 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 a4ca3ffaa..95e176064 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 4f84af5fe..fd442cdb4 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 cae644ab5..d1bcb0cf1 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 6674a8323..c104d0d15 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 8ae55d096..81590bd1c 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 5f772c591..86aa69681 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 6f2ff6ec4..0f4e8a588 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 f3c4a61e6..065cbe3ec 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 f042de00f..c85d51667 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 *)