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

17 files changed, 0 insertions, 93 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 8d0d0e78b..5068552d1 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -15,11 +15,8 @@ open Namegen
 open Term
 open Termops
 open Inductiveops
-open Sign
 open Environ
-open Inductive
 open Evd
-open Reduction
 open Typing
 open Pattern
 open Patternops
@@ -28,7 +25,6 @@ open Tacmach
 open Proof_type
 open Pfedit
 open Genredexpr
-open Evar_refiner
 open Tacred
 open Tactics
 open Tacticals
@@ -39,9 +35,7 @@ open Globnames
 open Nametab
 open Smartlocate
 open Libobject
-open Library
 open Printer
-open Declarations
 open Tacexpr
 open Mod_subst
 open Misctypes
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 00e8e1384..d2d18c53b 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -7,19 +7,15 @@
 (************************************************************************)
 
 open Equality
-open Hipattern
 open Names
 open Pp
 open Proof_type
 open Tacticals
-open Tacinterp
 open Tactics
 open Term
 open Termops
 open Errors
 open Util
-open Glob_term
-open Vernacinterp
 open Tacexpr
 open Mod_subst
 open Locus
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 3a0f1000f..e8cde2967 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -8,7 +8,6 @@
 
 open Term
 open Names
-open Termdn
 open Pattern
 open Globnames
 
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 6389e0d33..14a9ae9c2 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -6,17 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Errors
 open Term
-open Proof_type
 open Hipattern
 open Tacmach
 open Tacticals
 open Tactics
 open Coqlib
 open Reductionops
-open Glob_term
 open Misctypes
 
 (* Absurd *)
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 304b4117d..a2ec6dfa5 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -6,24 +6,16 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Errors
 open Util
 open Names
 open Term
 open Termops
-open Environ
-open Libnames
-open Reduction
 open Inductiveops
-open Proof_type
-open Clenv
 open Hipattern
 open Tacmach
 open Tacticals
 open Tactics
-open Hiddentac
-open Genarg
 open Tacexpr
 open Misctypes
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 16669b567..b4cb48285 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -11,7 +11,6 @@ open Errors
 open Util
 open Names
 open Nameops
-open Univ
 open Term
 open Termops
 open Namegen
@@ -21,26 +20,19 @@ open Environ
 open Libnames
 open Globnames
 open Reductionops
-open Typeops
 open Typing
 open Retyping
 open Tacmach
-open Proof_type
 open Logic
-open Evar_refiner
-open Pattern
 open Matching
 open Hipattern
 open Tacexpr
 open Tacticals
 open Tactics
 open Tacred
-open Glob_term
 open Coqlib
-open Vernacexpr
 open Declarations
 open Indrec
-open Printer
 open Clenv
 open Clenvtac
 open Evd
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index d2bc7fcf4..dd02adde1 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -6,16 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
-open Pp
 open Errors
 open Evar_refiner
 open Tacmach
 open Tacexpr
 open Refiner
-open Proof_type
 open Evd
-open Sign
 open Locus
 
 (* The instantiate tactic *)
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 9c7208a0e..77379cb74 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -6,13 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
-open Proof_type
-open Tacmach
 
-open Glob_term
 open Refiner
-open Genarg
 open Tacexpr
 open Tactics
 open Util
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 976947f2e..cb1ffb385 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -14,26 +14,16 @@ open Nameops
 open Term
 open Termops
 open Namegen
-open Global
-open Sign
 open Environ
 open Inductiveops
 open Printer
-open Reductionops
 open Retyping
 open Tacmach
-open Proof_type
-open Evar_refiner
 open Clenv
-open Tactics
 open Tacticals
 open Tactics
 open Elim
 open Equality
-open Typing
-open Pattern
-open Matching
-open Glob_term
 open Misctypes
 open Tacexpr
 
@@ -208,7 +198,6 @@ let split_dep_and_nodep hyps gl =
        if var_occurs_in_pf gl id then (d::l1,l2) else (l1,d::l2))
     hyps ([],[])
 
-open Coqlib
 
 (* Computation of dids is late; must have been done in rewrite_equations*)
 (* Will keep generalizing and introducing back and forth... *)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 9dc266ef1..5242d0f3e 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -10,7 +10,6 @@ open Pp
 open Errors
 open Util
 open Names
-open Nameops
 open Term
 open Termops
 open Namegen
@@ -18,21 +17,15 @@ open Sign
 open Evd
 open Printer
 open Reductionops
-open Declarations
 open Entries
 open Inductiveops
 open Environ
 open Tacmach
-open Proof_type
 open Pfedit
-open Evar_refiner
 open Clenv
 open Declare
 open Tacticals
 open Tactics
-open Inv
-open Vernacexpr
-open Safe_typing
 open Decl_kinds
 
 let no_inductive_inconstr env constr =
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index 83f65b274..5d5972089 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -6,12 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
 open Names
 open Term
-open Libobject
-open Library
 open Pattern
 open Globnames
 
diff --git a/tactics/refine.ml b/tactics/refine.ml
index b0705c024..fc2da8d0a 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -54,10 +54,7 @@ open Term
 open Termops
 open Namegen
 open Tacmach
-open Sign
 open Environ
-open Reduction
-open Typing
 open Tactics
 open Tacticals
 open Printer
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 459236fe5..b0997c067 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -8,9 +8,6 @@
 
 open Constrintern
 open Closure
-open RedFlags
-open Declarations
-open Entries
 open Libobject
 open Pattern
 open Patternops
@@ -19,7 +16,6 @@ open Pp
 open Genredexpr
 open Glob_term
 open Glob_ops
-open Sign
 open Tacred
 open Errors
 open Util
@@ -39,18 +35,13 @@ open Constrexpr_ops
 open Term
 open Termops
 open Tacexpr
-open Safe_typing
-open Typing
 open Hiddentac
 open Genarg
-open Decl_kinds
 open Mod_subst
 open Printer
 open Inductiveops
-open Syntax_def
 open Pretyping
 open Extrawit
-open Pcoq
 open Evd
 open Misctypes
 open Miscops
diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml
index b846c9eb7..7989b41db 100644
--- a/tactics/tactic_option.ml
+++ b/tactics/tactic_option.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Libobject
-open Proof_type
 open Pp
 
 let declare_tactic_option ?(default=Tacexpr.TacId []) name =
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 150e0050c..aaa75a4e2 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -14,20 +14,9 @@ open Term
 open Termops
 open Sign
 open Declarations
-open Inductive
-open Reduction
-open Environ
-open Libnames
-open Refiner
 open Tacmach
 open Clenv
 open Clenvtac
-open Glob_term
-open Pattern
-open Matching
-open Genarg
-open Tacexpr
-open Locus
 open Misctypes
 
 (************************************************************************)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 895b6dc35..1ccb3ffdb 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -16,7 +16,6 @@ open Term
 open Termops
 open Namegen
 open Declarations
-open Inductive
 open Inductiveops
 open Reductionops
 open Environ
@@ -28,14 +27,12 @@ open Genredexpr
 open Tacmach
 open Proof_type
 open Logic
-open Evar_refiner
 open Clenv
 open Clenvtac
 open Refiner
 open Tacticals
 open Hipattern
 open Coqlib
-open Nametab
 open Tacexpr
 open Decl_kinds
 open Evarutil
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index ff847ba6e..ffcde31ae 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -6,16 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
 open Names
-open Nameops
 open Term
 open Pattern
 open Patternops
-open Glob_term
 open Globnames
-open Nametab
 
 (* Discrimination nets of terms.
    See the module dn.ml for further explanations.