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

29 files changed, 0 insertions, 78 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 0970717ed..8af15a1d5 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -17,7 +17,6 @@ open Names
 open Term
 open Tacmach
 open Evd
-open Proof_type
 
 let init_size=5
 
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index d5eab32c4..25c01f2bd 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -10,7 +10,6 @@
 (* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
 
 open Errors
-open Util
 open Names
 open Term
 open Ccalgo
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 2042f9b05..53c146bfc 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -9,10 +9,7 @@
 (* This file is the interface between the c-c algorithm and Coq *)
 
 open Evd
-open Proof_type
 open Names
-open Libnames
-open Nameops
 open Inductiveops
 open Declarations
 open Term
@@ -21,12 +18,10 @@ open Tactics
 open Tacticals
 open Typing
 open Ccalgo
-open Tacinterp
 open Ccproof
 open Pp
 open Errors
 open Util
-open Format
 
 let constant dir s = lazy (Coqlib.gen_constant "CC" dir s)
 
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index e387b31a5..5e128bc42 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -11,7 +11,6 @@ open Util
 open Names
 open Constrexpr
 open Tacinterp
-open Tacmach
 open Decl_expr
 open Decl_mode
 open Pretyping
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 4fc5862c1..31e15081b 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -11,7 +11,6 @@ open Util
 open Pp
 open Evd
 
-open Refiner
 open Proof_type
 open Tacmach
 open Tacinterp
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index b72476a75..01f32e4a3 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Errors
-open Util
 open Pp
 open Decl_expr
 open Names
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 4b6bf39be..b6b7e5833 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -7,11 +7,8 @@
 (************************************************************************)
 
 open Pp
-open Errors
 open Util
 open Names
-open Term
-open Declarations
 open Namegen
 open Nameops
 open Libnames
@@ -19,8 +16,6 @@ open Globnames
 open Table
 open Miniml
 open Mlutil
-open Modutil
-open Mod_subst
 
 let string_of_id id =
   let s = Names.string_of_id id in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index ab0e480f9..0556f6d77 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 (*i*)
-open Errors
 open Util
 open Names
 open Term
@@ -20,9 +19,7 @@ open Termops
 open Inductiveops
 open Recordops
 open Namegen
-open Summary
 open Globnames
-open Nametab
 open Miniml
 open Table
 open Mlutil
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index a8c9375b1..3b89386d4 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -7,13 +7,10 @@
 (************************************************************************)
 
 (*i*)
-open Pp
-open Errors
 open Util
 open Names
 open Libnames
 open Globnames
-open Nametab
 open Table
 open Miniml
 (*i*)
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index d2e8e4951..1211bbf17 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -7,15 +7,12 @@
 (************************************************************************)
 
 open Names
-open Declarations
-open Environ
 open Globnames
 open Errors
 open Util
 open Miniml
 open Table
 open Mlutil
-open Mod_subst
 
 (*S Functions upon ML modules. *)
 
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 067c41705..34ae1f9ad 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -19,7 +19,6 @@ open Miniml
 open Mlutil
 open Modutil
 open Common
-open Declarations
 
 
 (*s Some utility functions. *)
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 27529258b..ec338b1db 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -12,8 +12,6 @@ open Pp
 open Errors
 open Util
 open Names
-open Nameops
-open Libnames
 open Miniml
 open Mlutil
 open Table
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 5cc7f61d9..7abb4dc52 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -10,13 +10,10 @@ open Hipattern
 open Names
 open Term
 open Termops
-open Reductionops
 open Tacmach
-open Errors
 open Util
 open Declarations
 open Globnames
-open Inductiveops
 
 let qflag=ref true
 
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 58bef84ea..753fdda72 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -12,9 +12,7 @@ open Rules
 open Instances
 open Term
 open Tacmach
-open Tactics
 open Tacticals
-open Libnames
 
 let update_flags ()=
   let predref=ref Names.Cpred.empty in
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index ee1c44265..e3367b4c2 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -6,11 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Formula
-open Sequent
 open Unify
 open Rules
-open Pp
 open Errors
 open Util
 open Term
@@ -20,7 +17,6 @@ open Tactics
 open Tacticals
 open Termops
 open Reductionops
-open Declarations
 open Formula
 open Sequent
 open Names
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 32c6030d1..37d9edef8 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -14,7 +14,6 @@ open Tacmach
 open Tactics
 open Tacticals
 open Termops
-open Declarations
 open Formula
 open Sequent
 open Globnames
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 7e6f65eaa..6d00e8d9f 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -12,7 +12,6 @@ open Util
 open Formula
 open Unify
 open Tacmach
-open Names
 open Globnames
 open Pp
 
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index ab18434de..33ea0ac8a 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -6,12 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
 open Util
-open Formula
-open Tacmach
 open Term
-open Names
 open Termops
 open Reductionops
 
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index b8887c68f..8ea4be631 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 cb41de283..e2dc149b0 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 93e1d105e..d11c01672 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 f678b898b..44ae42090 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 0ad8bc5e6..52562fb37 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 ff62a5c38..2817c549d 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 59090fb42..2f6a6a7d7 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 b848d77a7..4fe22a354 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 3176ae34a..14d9b7fcb 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
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index de9dca939..8f34ec495 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -9,21 +9,11 @@
 (* This file defines the printer for natural numbers in [nat] *)
 
 (*i*)
-open Pcoq
-open Pp
-open Errors
-open Util
-open Names
-open Coqlib
 open Glob_term
-open Libnames
 open Bigint
 open Coqlib
-open Notation
 open Pp
 open Errors
-open Util
-open Names
 (*i*)
 
 (**********************************************************************)
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 1ff28dd79..7cad42d60 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -6,13 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pcoq
 open Pp
 open Errors
-open Util
 open Names
-open Topconstr
-open Libnames
 open Bigint
 
 exception Non_closed_number
@@ -21,7 +17,6 @@ exception Non_closed_number
 (* Parsing positive via scopes                                        *)
 (**********************************************************************)
 
-open Libnames
 open Globnames
 open Glob_term