22 files changed, 0 insertions, 40 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 7a40a40297..098da5184a 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -10,8 +10,6 @@
    machine, Oct 2004 *)
 (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
 
-open Errors
-open Util
 open Names
 open Cbytecodes
 open Cemitcodes
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 11b9b4de9e..94980b5964 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -24,7 +24,6 @@ open Util
 open Pp
 open Term
 open Names
-open Declarations
 open Environ
 open Esubst
 
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index d016d7f63b..a015cdf927 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -13,15 +13,12 @@
 (* This module implements kernel-level discharching of local
    declarations over global constants and inductive types *)
 
-open Pp
 open Errors
-open Util
 open Names
 open Term
 open Sign
 open Declarations
 open Environ
-open Reduction
 
 (*s Cooking the constants. *)
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 9dec5887c5..5f677d0565 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -21,7 +21,6 @@
    global constants/axioms, mutual inductive definitions and the
    module system *)
 
-open Errors
 open Util
 open Names
 open Univ
diff --git a/kernel/entries.ml b/kernel/entries.ml
index f17918a6c5..2da2c78994 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -8,7 +8,6 @@
 
 (*i*)
 open Names
-open Univ
 open Term
 open Sign
 (*i*)
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index c1311ac90f..0bd7c515c6 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -10,7 +10,6 @@
 
 (* Support for explicit substitutions *)
 
-open Errors
 open Util
 
 (*********************)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 690d5e6860..6c7f4408f7 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -13,7 +13,6 @@ open Univ
 open Term
 open Declarations
 open Inductive
-open Sign
 open Environ
 open Reduction
 open Typeops
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 748ccf838e..58689a9263 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -11,7 +11,6 @@ open Util
 open Names
 open Univ
 open Term
-open Sign
 open Declarations
 open Environ
 open Reduction
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index a9d4d88325..e7a5227e05 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -14,7 +14,6 @@
    substitution in module constructions *)
 
 open Pp
-open Errors
 open Util
 open Names
 open Term
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 03ee613329..d9f3c3bf0a 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -13,13 +13,11 @@
    declarations *)
 
 open Errors
-open Util
 open Names
 open Univ
 open Declarations
 open Entries
 open Environ
-open Term_typing
 open Modops
 open Subtyping
 open Mod_subst
diff --git a/kernel/modops.ml b/kernel/modops.ml
index cd3bc1513d..5eddb6c843 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -16,10 +16,7 @@
 (* This file provides with various operations on modules and module types *)
 
 open Errors
-open Util
-open Pp
 open Names
-open Univ
 open Term
 open Declarations
 open Environ
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 485b1ecaff..3d2f19aac8 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -13,8 +13,6 @@
 
 (* This file defines the type of kernel environments *)
 
-open Errors
-open Util
 open Names
 open Sign
 open Univ
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 02ffab643a..4ce3e7f225 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -20,7 +20,6 @@ open Util
 open Names
 open Term
 open Univ
-open Declarations
 open Environ
 open Closure
 open Esubst
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 58bae94d66..4dc01f890f 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -14,7 +14,6 @@
    for evaluation in the bytecode virtual machine *)
 
 open Term
-open Names
 
 (* Type declarations, these types shouldn't be exported they are accessed
    through specific functions. As being mutable and all it is wiser *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c154cba407..11d647d9aa 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -58,19 +58,12 @@
 *)
 
 open Errors
-open Util
 open Names
 open Univ
-open Term
-open Reduction
-open Sign
 open Declarations
-open Inductive
 open Environ
 open Entries
 open Typeops
-open Type_errors
-open Indtypes
 open Term_typing
 open Modops
 open Subtyping
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 18ef1bd3f0..a654bc04dd 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -16,7 +16,6 @@
    names-based contexts *)
 
 open Names
-open Errors
 open Util
 open Term
 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 961dd652fa..5fec0c2c7e 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -12,18 +12,15 @@
 (* This module checks subtyping of module types *)
 
 (*i*)
-open Errors
 open Util
 open Names
 open Univ
 open Term
 open Declarations
-open Environ
 open Reduction
 open Inductive
 open Modops
 open Mod_subst
-open Entries
 (*i*)
 
 (* This local type is used to subtype a constant with a constructor or
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index dbd22e559d..aed7615b80 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -17,13 +17,9 @@ open Util
 open Names
 open Univ
 open Term
-open Reduction
-open Sign
 open Declarations
-open Inductive
 open Environ
 open Entries
-open Type_errors
 open Indtypes
 open Typeops
 
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 890f0976ed..6d4b420262 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Sign
 open Environ
 open Reduction
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 608bcc886c..3ec08fef48 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -12,7 +12,6 @@ open Names
 open Univ
 open Term
 open Declarations
-open Sign
 open Environ
 open Entries
 open Reduction
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 4d0edc689e..7044b13726 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -1,5 +1,4 @@
 open Names
-open Declarations
 open Term
 open Environ
 open Conv_oracle
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 5e21db2143..656e555fc9 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Conv_oracle
 open Cbytecodes
 
 external set_drawinstr : unit -> unit = "coq_set_drawinstr"