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

9 files changed, 0 insertions, 21 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index b8887c68f9..8ea4be631c 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -6,9 +6,7 @@ open Namegen
 open Names
 open Declarations
 open Pp
-open Entries
 open Hiddentac
-open Evd
 open Tacmach
 open Proof_type
 open Tacticals
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index cb41de283a..e2dc149b09 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -7,11 +7,6 @@ open Names
 open Declarations
 open Pp
 open Entries
-open Hiddentac
-open Evd
-open Tacmach
-open Proof_type
-open Tacticals
 open Tactics
 open Indfun_common
 open Functional_principles_proofs
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 93e1d105e6..d11c01672a 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -4,7 +4,6 @@ open Names
 open Term
 open Glob_term
 open Glob_ops
-open Libnames
 open Globnames
 open Indfun_common
 open Errors
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index f678b898ba..44ae420904 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -1,7 +1,6 @@
 open Pp
 open Glob_term
 open Errors
-open Util
 open Names
 open Decl_kinds
 open Misctypes
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 0ad8bc5e6d..52562fb374 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -695,7 +695,6 @@ let do_generate_principle on_error register_built interactive_proof
   in
   ()
 
-open Topconstr
 let rec add_args id new_args b =
   match b with
   | CRef r ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index ff62a5c385..2817c549dd 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -149,7 +149,6 @@ let refl_equal = lazy(coq_constant "eq_refl")
 (* Copy of the standart save mechanism but without the much too  *)
 (* slow reduction function                                       *)
 (*****************************************************************)
-open Declarations
 open Entries
 open Decl_kinds
 open Declare
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 59090fb421..2f6a6a7d7b 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -12,13 +12,11 @@ open Util
 open Names
 open Term
 open Pp
-open Libnames
 open Globnames
 open Tacticals
 open Tactics
 open Indfun_common
 open Tacmach
-open Sign
 open Hiddentac
 open Misctypes
 
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index b848d77a72..4fe22a3543 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -8,7 +8,6 @@
 
 (* Merging of induction principles. *)
 
-open Libnames
 open Globnames
 open Tactics
 open Indfun_common
@@ -21,7 +20,6 @@ open Names
 open Term
 open Termops
 open Declarations
-open Environ
 open Glob_term
 open Glob_termops
 open Decl_kinds
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 3176ae34aa..14d9b7fcb0 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Tacexpr
 open Term
 open Namegen
 open Environ
@@ -20,9 +19,7 @@ open Nameops
 open Errors
 open Util
 open Closure
-open RedFlags
 open Tacticals
-open Typing
 open Tacmach
 open Tactics
 open Nametab
@@ -31,12 +28,9 @@ open Declare
 open Decl_kinds
 open Tacred
 open Proof_type
-open Vernacinterp
 open Pfedit
-open Topconstr
 open Glob_term
 open Pretyping
-open Safe_typing
 open Constrintern
 open Hiddentac
 open Misctypes