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.

10 files changed, 3 insertions, 26 deletions

diff --git a/library/assumptions.mli b/library/assumptions.mli
index cd08caf73..2e5810935 100644
--- a/library/assumptions.mli
+++ b/library/assumptions.mli
@@ -9,7 +9,6 @@
 open Util
 open Names
 open Term
-open Environ
 
 (** A few declarations for the "Print Assumption" command
     @author spiwack *)
diff --git a/library/declare.mli b/library/declare.mli
index f33077ddb..663d240dc 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -9,12 +9,7 @@
 open Names
 open Libnames
 open Term
-open Context
-open Declarations
 open Entries
-open Indtypes
-open Safe_typing
-open Nametab
 open Decl_kinds
 
 (** This module provides the official functions to declare new variables,
@@ -24,8 +19,6 @@ open Decl_kinds
    reset works properly --- and will fill some global tables such as
    [Nametab] and [Impargs]. *)
 
-open Nametab
-
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
 type section_variable_entry =
diff --git a/library/decls.mli b/library/decls.mli
index 001d060e8..f45e4f121 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Context
 open Libnames
 open Decl_kinds
 
diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli
index f2173bf49..884ba6a78 100644
--- a/library/dischargedhypsmap.mli
+++ b/library/dischargedhypsmap.mli
@@ -7,9 +7,6 @@
 (************************************************************************)
 
 open Libnames
-open Term
-open Environ
-open Nametab
 
 type discharged_hyps = full_path list
 
diff --git a/library/globnames.mli b/library/globnames.mli
index 4bf21cf0a..7afe80150 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Util
-open Pp
 open Names
 open Term
 open Mod_subst
diff --git a/library/goptions.mli b/library/goptions.mli
index 6f23cf5ea..6251b8d2d 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -44,10 +44,7 @@
    (synchronous = consistent with the resetting commands)                   *)
 
 open Pp
-open Names
 open Libnames
-open Term
-open Nametab
 open Mod_subst
 
 type option_name = Interface.option_name
diff --git a/library/impargs.mli b/library/impargs.mli
index 4fb056986..e70cff838 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -10,7 +10,6 @@ open Names
 open Globnames
 open Term
 open Environ
-open Nametab
 
 (** {6 Implicit Arguments } *)
 (** Here we store the implicit arguments. Notice that we
diff --git a/library/libobject.ml b/library/libobject.ml
index 3bbb1e90e..9c46b886d 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -6,10 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
-open Errors
 open Libnames
-open Mod_subst
 
 (* The relax flag is used to make it possible to load files while ignoring
    failures to incorporate some objects.  This can be useful when one
@@ -32,11 +29,11 @@ type 'a object_declaration = {
   load_function : int -> object_name * 'a -> unit;
   open_function : int -> object_name * 'a -> unit;
   classify_function : 'a -> 'a substitutivity;
-  subst_function :  substitution * 'a -> 'a;
+  subst_function : Mod_subst.substitution * 'a -> 'a;
   discharge_function : object_name * 'a -> 'a option;
   rebuild_function : 'a -> 'a }
 
-let yell s = anomaly (Pp.str s)
+let yell s = Errors.anomaly (Pp.str s)
 
 let default_object s = {
   object_name = s;
@@ -69,7 +66,7 @@ type dynamic_object_declaration = {
   dyn_cache_function : object_name * obj -> unit;
   dyn_load_function : int -> object_name * obj -> unit;
   dyn_open_function : int -> object_name * obj -> unit;
-  dyn_subst_function : substitution * obj -> obj;
+  dyn_subst_function : Mod_subst.substitution * obj -> obj;
   dyn_classify_function : obj -> obj substitutivity;
   dyn_discharge_function : object_name * obj -> obj option;
   dyn_rebuild_function : obj -> obj }
diff --git a/library/libobject.mli b/library/libobject.mli
index 3986b3d3f..3dfc1e5ef 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Libnames
 open Mod_subst
 
diff --git a/library/library.mli b/library/library.mli
index 69fd5e940..afcce7f6c 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -7,10 +7,8 @@
 (************************************************************************)
 
 open Loc
-open Pp
 open Names
 open Libnames
-open Libobject
 
 (** This module provides functions to load, open and save
   libraries. Libraries correspond to the subclass of modules that