Remove many superfluous 'open' indicated by ocamlc -w +33

 With ocaml 4.01, the 'unused open' warning also checks the mli :-)

 Beware: some open are reported as useless when compiling with camlp5,
 but are necessary for compatibility with camlp4. These open are now
 marked with a comment.

31 files changed, 0 insertions, 98 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 9bb55977ec..795582f278 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -30,13 +30,11 @@ open Tacticals
 open Clenv
 open Libnames
 open Globnames
-open Nametab
 open Smartlocate
 open Libobject
 open Printer
 open Tacexpr
 open Mod_subst
-open Misctypes
 open Locus
 open Proofview.Notations
 
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 7ce351f434..2d27208805 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -32,8 +32,6 @@ type 'a auto_tactic =
   | Unfold_nth of evaluable_global_reference          (** Hint Unfold *)
   | Extern     of Tacexpr.glob_tactic_expr   (** Hint Extern *)
 
-open Glob_term
-
 type hints_path_atom = 
   | PathHints of global_reference list
   | PathAny
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index c5017ac75b..ba36761459 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -9,7 +9,6 @@
 open Equality
 open Names
 open Pp
-open Proof_type
 open Tacticals
 open Tactics
 open Term
@@ -19,7 +18,6 @@ open Util
 open Tacexpr
 open Mod_subst
 open Locus
-open Proofview.Notations
 
 (* Rewriting rules *)
 type rew_rule = { rew_lemma: constr;
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 69ab9c55f2..198fa36f59 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -8,7 +8,6 @@
 
 open Term
 open Tacexpr
-open Tacmach
 open Equality
 
 (** Rewriting rules before tactic interpretation *)
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index c6fb0d12aa..13c188c79e 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -15,7 +15,6 @@ open Tactics
 open Coqlib
 open Reductionops
 open Misctypes
-open Proofview.Notations
 
 (* Absurd *)
 
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
index e3dabfe983..8ec6de88a0 100644
--- a/tactics/contradiction.mli
+++ b/tactics/contradiction.mli
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Term
-open Proof_type
 open Misctypes
 
 val absurd                      : constr -> unit Proofview.tactic
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index ba35433f19..e2da23aaaf 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -8,12 +8,8 @@
 
 open Term
 open Proof_type
-open Tacexpr
 open Auto
-open Topconstr
 open Evd
-open Environ
-open Explore
 
 val hintbases : hint_db_name list option Pcoq.Gram.entry
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 06f84ecd1e..5d5b592ad4 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
 open Util
 open Names
 open Term
diff --git a/tactics/elim.mli b/tactics/elim.mli
index 35b7b26025..b83a97bccb 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -8,9 +8,6 @@
 
 open Names
 open Term
-open Proof_type
-open Tacmach
-open Genarg
 open Tacticals
 open Misctypes
 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 24c9095813..e8b142d89c 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -7,22 +7,13 @@
 (************************************************************************)
 
 (*i*)
-open Pp
 open Names
 open Term
 open Context
 open Evd
 open Environ
-open Proof_type
 open Tacmach
-open Hipattern
-open Pattern
-open Tacticals
-open Tactics
 open Tacexpr
-open Termops
-open Glob_term
-open Genarg
 open Ind_tables
 open Locus
 open Misctypes
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 20f72b3d56..83a98745af 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Util
-open Names
 open Errors
 open Evar_refiner
 open Tacmach
@@ -50,7 +49,6 @@ let instantiate n (ist,rawc) ido gl =
         tclNORMEVAR
         gl
 
-open Proofview.Notations
 let let_evar name typ =
   let src = (Loc.ghost,Evar_kinds.GoalEvar) in
   Proofview.Goal.enter begin fun gl ->
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index dfc14bddf3..16c236b822 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -7,11 +7,8 @@
 (************************************************************************)
 
 open Tacexpr
-open Term
 open Names
-open Proof_type
 open Constrexpr
-open Termops
 open Glob_term
 open Misctypes
 
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 2b28a65471..69ef3b4ddb 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Proof_type
-
 val discrHyp : Names.Id.t -> unit Proofview.tactic
 val injHyp : Names.Id.t -> unit Proofview.tactic
 
diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4
index c7867a83c8..6012088f7b 100644
--- a/tactics/g_class.ml4
+++ b/tactics/g_class.ml4
@@ -17,8 +17,6 @@ END
 
 (** Options: depth, debug and transparency settings. *)
 
-open Goptions
-
 let set_transparency cl b =
   List.iter (fun r ->
     let gr = Smartlocate.global_with_alias r in
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index 03bbc4b046..954892e81d 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -11,19 +11,14 @@
 (* Syntax for rewriting with strategies *)
 
 open Names
-open Term
-open Vars
 open Misctypes
 open Locus
-open Locusops
 open Constrexpr
 open Glob_term
-open Patternops
 open Geninterp
 open Extraargs
 open Tacmach
 open Tacticals
-open Tactics
 open Rewrite
 
 type constr_expr_with_bindings = constr_expr with_bindings
diff --git a/tactics/geninterp.ml b/tactics/geninterp.ml
index e9d3f42925..4a49ae287f 100644
--- a/tactics/geninterp.ml
+++ b/tactics/geninterp.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
-open Util
 open Names
 open Genarg
 
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index b38eb654be..4735b26b32 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -8,9 +8,7 @@
 
 open Names
 open Term
-open Context
 open Evd
-open Pattern
 open Coqlib
 
 (** High-order patterns *)
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 9491b7d7b9..f5820c33cb 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -7,13 +7,10 @@
 (************************************************************************)
 
 open Loc
-open Pp
 open Names
 open Term
-open Tacmach
 open Misctypes
 open Tacexpr
-open Glob_term
 
 type inversion_status = Dep of constr option | NoDep
 
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 7af7fcb025..ac56e6688b 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -28,7 +28,6 @@ open Declare
 open Tacticals
 open Tactics
 open Decl_kinds
-open Proofview.Notations
 
 let no_inductive_inconstr env constr =
   (str "Cannot recognize an inductive predicate in " ++
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 16695fcd7d..36aa5e67f2 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -7,11 +7,8 @@
 (************************************************************************)
 
 open Loc
-open Pp
 open Names
 open Term
-open Glob_term
-open Proof_type
 open Constrexpr
 open Misctypes
 
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 853215a5ab..79a1a41c8d 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -8,34 +8,28 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open Pp
 open Errors
 open Util
-open Names
 open Nameops
 open Namegen
 open Term
 open Vars
-open Termops
 open Reduction
 open Tacticals
 open Tacmach
 open Tactics
 open Patternops
 open Clenv
-open Glob_term
 open Typeclasses
 open Typeclasses_errors
 open Classes
 open Constrexpr
-open Libnames
 open Globnames
 open Evd
 open Misctypes
 open Locus
 open Locusops
 open Decl_kinds
-open Tacinterp
 open Elimschemes
 open Goal
 open Environ
@@ -43,8 +37,6 @@ open Pp
 open Names
 open Tacinterp
 open Termops
-open Genarg
-open Extraargs
 open Entries
 open Libnames
 
@@ -1345,8 +1337,6 @@ let occurrences_of = function
 	error "Illegal negative occurrence number.";
       (true,nl)
 
-open Extraargs
-
 let apply_glob_constr c l2r occs = fun () env avoid t ty cstr evars ->
   let evd, c = (Pretyping.understand_tcc (goalevars evars) env c) in
     apply_lemma l2r (general_rewrite_unif_flags ()) (c, NoBindings)
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index aa254c2f86..2c1de14ea9 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Util
-open Errors
 open Names
 open Term
 open Pattern
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index c787ebbda8..9b50cc1c02 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Libobject
 open Pattern
 open Pp
 open Genredexpr
@@ -21,12 +20,10 @@ open Globnames
 open Nametab
 open Smartlocate
 open Constrexpr
-open Constrexpr_ops
 open Termops
 open Tacexpr
 open Genarg
 open Constrarg
-open Mod_subst
 open Misctypes
 open Locus
 
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
index 8473f585bd..22588fcf16 100644
--- a/tactics/tacintern.mli
+++ b/tactics/tacintern.mli
@@ -8,15 +8,9 @@
 
 open Pp
 open Names
-open Proof_type
-open Tacmach
-open Tactic_debug
-open Term
 open Tacexpr
 open Genarg
 open Constrexpr
-open Mod_subst
-open Redexpr
 open Misctypes
 open Nametab
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0e802f8a9c..60564dbdb7 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Constrintern
-open Pattern
 open Patternops
 open Pp
 open Genredexpr
@@ -37,7 +36,6 @@ open Printer
 open Pretyping
 open Evd
 open Misctypes
-open Miscops
 open Locus
 open Tacintern
 open Taccoerce
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 0c89eb3a28..49d40db240 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -6,16 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
-open Proof_type
-open Tacmach
 open Tactic_debug
 open Term
 open Tacexpr
 open Genarg
-open Constrexpr
-open Mod_subst
 open Redexpr
 open Misctypes
 
diff --git a/tactics/tactic_option.mli b/tactics/tactic_option.mli
index be36b3f82d..db437ce0c9 100644
--- a/tactics/tactic_option.mli
+++ b/tactics/tactic_option.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Proof_type
 open Tacexpr
 open Vernacexpr
 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 310023e544..3e6e64ecb5 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -14,12 +14,7 @@ open Context
 open Tacmach
 open Proof_type
 open Clenv
-open Reduction
-open Pattern
-open Genarg
 open Tacexpr
-open Termops
-open Glob_term
 open Locus
 open Misctypes
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a5f88c9291..fda84e6f59 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -26,7 +26,6 @@ open Pfedit
 open Tacred
 open Genredexpr
 open Tacmach
-open Proof_type
 open Logic
 open Clenv
 open Clenvtac
@@ -43,7 +42,6 @@ open Unification
 open Locus
 open Locusops
 open Misctypes
-open Miscops
 open Proofview.Notations
 
 exception Bound
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b181dc5348..9f4f0e9ce1 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -7,26 +7,17 @@
 (************************************************************************)
 
 open Loc
-open Pp
 open Names
 open Term
 open Context
 open Environ
-open Tacmach
 open Proof_type
-open Reduction
 open Evd
-open Evar_refiner
 open Clenv
 open Redexpr
-open Tacticals
 open Globnames
-open Genarg
 open Tacexpr
-open Nametab
-open Glob_term
 open Pattern
-open Termops
 open Unification
 open Misctypes
 open Locus
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 05a08c8253..2a35e32d97 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -15,7 +15,6 @@ open Globnames
 open Pp
 open Genarg
 open Stdarg
-open Tacticals
 open Tacinterp
 open Tactics
 open Errors