This patch removes unused "open" (automatically generated from

compiler warnings).

I was afraid that such a brutal refactoring breaks some obscure
invariant about linking order and side-effects but the standard
library still compiles.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7

22 files changed, 0 insertions, 40 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 7a40a4029..098da5184 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 11b9b4de9..94980b596 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 d016d7f63..a015cdf92 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 9dec5887c..5f677d056 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 f17918a6c..2da2c7899 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 c1311ac90..0bd7c515c 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 690d5e686..6c7f4408f 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 748ccf838..58689a926 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 a9d4d8832..e7a5227e0 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 03ee61332..d9f3c3bf0 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 cd3bc1513..5eddb6c84 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 485b1ecaf..3d2f19aac 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 02ffab643..4ce3e7f22 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 58bae94d6..4dc01f890 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 c154cba40..11d647d9a 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 18ef1bd3f..a654bc04d 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 961dd652f..5fec0c2c7 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 dbd22e559..aed7615b8 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 890f0976e..6d4b42026 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 608bcc886..3ec08fef4 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 4d0edc689..7044b1372 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 5e21db214..656e555fc 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"