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.

25 files changed, 0 insertions, 63 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index b79d774431..94447f0d04 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -21,7 +21,6 @@ open Names
 open Globnames
 open Inductiveops
 open Tactics
-open Tacticals
 open Ind_tables
 open Misctypes
 open Proofview.Notations
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli
index 660f6f7e72..6509a7d3b8 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.mli
@@ -8,10 +8,6 @@
 
 open Term
 open Names
-open Libnames
-open Mod_subst
-open Context
-open Proof_type
 open Ind_tables
 
 (** This file is about the automatic generation of schemes about
diff --git a/toplevel/autoinstance.mli b/toplevel/autoinstance.mli
index ebaaee12d0..bfc9bcff27 100644
--- a/toplevel/autoinstance.mli
+++ b/toplevel/autoinstance.mli
@@ -8,8 +8,6 @@
 
 open Term
 open Globnames
-open Typeclasses
-open Names
 open Evd
 open Context
 
diff --git a/toplevel/class.mli b/toplevel/class.mli
index 0d39ee1709..8bb3eb7ce8 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -7,12 +7,8 @@
 (************************************************************************)
 
 open Names
-open Term
 open Classops
-open Declare
 open Globnames
-open Decl_kinds
-open Nametab
 
 (** Classes and coercions. *)
 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 220e0e0506..4d8a6d5d78 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -10,8 +10,6 @@
 open Names
 open Term
 open Vars
-open Context
-open Evd
 open Environ
 open Nametab
 open Errors
@@ -26,7 +24,6 @@ open Constrexpr
 
 open Decl_kinds
 open Entries
-open Misctypes
 
 let typeclasses_db = "typeclass_instances"
 
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index a8e611928e..de62ff369e 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -7,18 +7,12 @@
 (************************************************************************)
 
 open Names
-open Decl_kinds
-open Term
 open Context
 open Evd
 open Environ
-open Nametab
-open Mod_subst
 open Constrexpr
 open Typeclasses
-open Implicit_quantifiers
 open Libnames
-open Globnames
 
 (** Errors *)
 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index fe6a0a4003..d2ebdc5611 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
 open Term
 open Entries
@@ -17,7 +16,6 @@ open Vernacexpr
 open Constrexpr
 open Decl_kinds
 open Redexpr
-open Constrintern
 open Pfedit
 
 (** This file is about the interpretation of raw commands into typed
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 1375f33619..4aedaa0352 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Pcoq
 
 (** The Coq toplevel loop. *)
 
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index 6f696f27a0..6cef31c8a8 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Context
-open Cooking
 open Declarations
 open Entries
 open Opaqueproof
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 5d024d31c5..303b3f8d65 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -14,7 +14,6 @@ open Namegen
 open Term
 open Termops
 open Indtypes
-open Context
 open Environ
 open Pretype_errors
 open Type_errors
@@ -24,9 +23,6 @@ open Cases
 open Logic
 open Printer
 open Evd
-open Libnames
-open Globnames
-open Declarations
 
 (* This simplifies the typing context of Cases clauses *)
 (* hope it does not disturb other typing contexts *)
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 9ec3444059..bdc3eb7070 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Names
 open Indtypes
 open Environ
 open Type_errors
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index c5e82e2e2f..d57f1556d7 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -8,10 +8,6 @@
 
 open Term
 open Names
-open Libnames
-open Mod_subst
-open Context
-open Declarations
 
 (** This module provides support for registering inductive scheme builders,
    declaring schemes and generating schemes on demand *)
diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli
index be49f41e54..7abae933dd 100644
--- a/toplevel/indschemes.mli
+++ b/toplevel/indschemes.mli
@@ -7,15 +7,10 @@
 (************************************************************************)
 
 open Loc
-open Pp
 open Names
 open Term
 open Environ
-open Libnames
-open Glob_term
-open Genarg
 open Vernacexpr
-open Ind_tables
 open Misctypes
 
 (** See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ... *)
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index f6cf147ab0..fd606a6b88 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -27,12 +27,10 @@ open Declare
 open Pretyping
 open Termops
 open Namegen
-open Evarutil
 open Reductionops
 open Constrexpr
 open Constrintern
 open Impargs
-open Tacticals
 
 (* Support for mutually proved theorems *)
 
diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli
index aea5c95cf5..bbe383a857 100644
--- a/toplevel/lemmas.mli
+++ b/toplevel/lemmas.mli
@@ -12,7 +12,6 @@ open Decl_kinds
 open Constrexpr
 open Tacexpr
 open Vernacexpr
-open Proof_type
 open Pfedit
 
 (** A hook start_proof calls on the type of the definition being started *)
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 93752b3bcf..20326c9c8d 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Libnames
 open Tacexpr
 open Vernacexpr
 open Notation
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 6536796f4e..d772af3c18 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -20,7 +20,6 @@ open Evd
 open Pp
 open Errors
 open Util
-open Proof_type
 
 let declare_fix_ref = ref (fun _ _ _ _ _ -> assert false)
 let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
@@ -143,9 +142,6 @@ let etype_of_evar evs hyps concl =
 	  subst_vars acc 0 t', s, trans
   in aux [] 0 (List.rev hyps)
 
-
-open Tacticals
-
 let trunc_named_context n ctx =
   let len = List.length ctx in
     List.firstn (len - n) ctx
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 04292422cc..746b4ed14d 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -7,15 +7,11 @@
 (************************************************************************)
 
 open Environ
-open Tacmach
 open Term
 open Evd
 open Names
 open Pp
-open Util
-open Tacinterp
 open Globnames
-open Proof_type
 open Vernacexpr
 open Decl_kinds
 open Tacexpr
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 78fa3a325d..72528675c9 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Errors
 open Util
 open Names
 open Term
diff --git a/toplevel/search.mli b/toplevel/search.mli
index c139c71cd8..c06a64be17 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -12,7 +12,6 @@ open Term
 open Environ
 open Pattern
 open Globnames
-open Nametab
 
 (** {6 Search facilities. } *)
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index b35929fef2..667a600582 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -14,7 +14,6 @@ open Util
 open Flags
 open System
 open Vernacexpr
-open Vernacinterp
 
 (* The functions in this module may raise (unexplainable!) exceptions.
    Use the module Coqtoplevel, which catches these exceptions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index cd38510f32..3951190832 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -30,7 +30,6 @@ open Decl_kinds
 open Constrexpr
 open Redexpr
 open Lemmas
-open Declaremods
 open Misctypes
 open Locality
 
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 3f6d45a049..9b49e57720 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -6,11 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
-open Term
-open Vernacinterp
-open Vernacexpr
-open Constrexpr
 open Misctypes
 
 val dump_global : Libnames.reference or_by_notation -> unit
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 8f8f5bdd7f..3cbbbf05ee 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Tacexpr
-
 (** Interpretation of extended vernac phrases. *)
 
 val vinterp_add : string -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit
diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli
index fed8332bd8..ab8069ec61 100644
--- a/toplevel/whelp.mli
+++ b/toplevel/whelp.mli
@@ -11,8 +11,6 @@
 
 open Names
 open Term
-open Topconstr
-open Environ
 
 type whelp_request =
   | Locate of string