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.

17 files changed, 0 insertions, 36 deletions

diff --git a/kernel/closure.mli b/kernel/closure.mli
index 161de91cf..19baedf27 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
 open Term
 open Environ
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 826c7f643..cf05fe013 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -23,12 +23,8 @@
    Inductive Constructions (CIC) terms together with constructors,
    destructors, iterators and basic functions *)
 
-open Errors
 open Util
-open Pp
 open Names
-open Univ
-open Esubst
 
 
 type existential_key = Evar.t
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index f8724180e..31e86e854 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -17,7 +17,6 @@ open Errors
 open Util
 open Names
 open Term
-open Context
 open Declarations
 open Environ
 
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 8493b81d8..030e88829 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -6,11 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Term
 open Declarations
 open Environ
-open Univ
 
 (** {6 Cooking the constants. } *)
 
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index ce789b00e..016a1a5b5 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -7,12 +7,10 @@
 (************************************************************************)
 
 open Names
-open Univ
 open Term
 open Declarations
 open Environ
 open Entries
-open Typeops
 
 (** Inductive type checking and errors *)
 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 2bd421bb3..188bff626 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -15,7 +15,6 @@
 
 (* This file provides with various operations on modules and module types *)
 
-open Errors
 open Util
 open Names
 open Term
diff --git a/kernel/modops.mli b/kernel/modops.mli
index f50dcfd63..a71e28d6e 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Univ
 open Term
 open Environ
 open Declarations
diff --git a/kernel/names.ml b/kernel/names.ml
index 047d8a88d..3de12b1bc 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -19,7 +19,6 @@
    Élie Soubiran, ... *)
 
 open Pp
-open Errors
 open Util
 
 (** {6 Identifiers } *)
@@ -485,8 +484,6 @@ module KerPair = struct
       the same user part implies having the same canonical part
       (invariant of the system). *)
 
-  open Hashset.Combine
-
   let hash = function
   | Same kn -> KerName.hash kn
   | Dual (kn, _) -> KerName.hash kn
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 3435e1d75..82786df64 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -7,15 +7,11 @@
 (************************************************************************)
 open Errors
 open Names
-open Term
 open Univ
-open Pre_env
 open Nativelib
 open Reduction
-open Declarations
 open Util
 open Nativevalues
-open Nativelambda
 open Nativecode 
 
 (** This module implements the conversion test by compiling to OCaml code *)
diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli
index 248130076..69b9d22ec 100644
--- a/kernel/nativeconv.mli
+++ b/kernel/nativeconv.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 open Term
-open Univ
-open Environ
 open Reduction
 open Nativelambda
 
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 860283e06..98314348a 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -5,11 +5,8 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-open Util
 open Names
-open Esubst
 open Term
-open Declarations
 open Pre_env
 open Nativevalues
 
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index f8c39b4dc..a69b9d472 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -5,13 +5,9 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-open Names
-open Term
 open Util
 open Nativevalues
-open Declarations
 open Nativecode
-open Pre_env
 open Errors
 open Envars
 
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index 0cbe4ccd5..9ef8c06a3 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -5,11 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-open Names
-open Term
-open Nativevalues
 open Nativecode
-open Pre_env
 
 (** This file provides facilities to access OCaml compiler and dynamic linker,
 used by the native compiler. *)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 2d117cc96..7c0607cc4 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -9,7 +9,6 @@
 open Term
 open Context
 open Environ
-open Closure
 
 (***********************************************************************
   s Reduction functions *)
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 6b76e616a..ea2b3de24 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Term
 
 type retroknowledge
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index 4168e5016..96ab5adec 100644
--- a/kernel/vconv.mli
+++ b/kernel/vconv.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Term
 open Environ
 open Reduction
diff --git a/kernel/vm.mli b/kernel/vm.mli
index cbc68c488..fa88418ce 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -1,7 +1,6 @@
 open Names
 open Term
 open Cbytecodes
-open Cemitcodes
 
 (** Efficient Virtual Machine *)