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.

16 files changed, 0 insertions, 44 deletions

diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index c8b63ea0f..7731c4ca2 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -6,14 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Term
-open Context
 open Environ
 open Evd
-open Evarutil
 open Mod_subst
-open Glob_term
 open Unification
 open Misctypes
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index f852995a0..29211c71a 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -83,7 +83,6 @@ let elim_res_pf_THEN_i clenv tac gls =
   let clenv' = (clenv_unique_resolver ~flags:elim_flags clenv gls) in
   tclTHENLASTn (clenv_refine false clenv') (tac clenv') gls
 
-open Proofview.Notations
 let new_elim_res_pf_THEN_i clenv tac =
   Proofview.Goal.enter begin fun gl ->
     let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags:elim_flags clenv) gl in
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index d172d5c36..86d567ef2 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -6,10 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Term
-open Context
-open Evd
 open Clenv
 open Proof_type
 open Tacexpr
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 6eee974d9..d5b80398a 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -6,13 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
-open Term
-open Environ
 open Evd
-open Refiner
 open Pretyping
-open Glob_term
 
 (** Refinement of existential variables. *)
 
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 69c10812a..da54ef0a8 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -8,9 +8,7 @@
 
 open Names
 open Term
-open Context
 open Evd
-open Environ
 open Proof_type
 
 (** This suppresses check done in [prim_refiner] for the tactic given in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index f0ea69533..ca760c456 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -12,7 +12,6 @@ open Names
 open Entries
 open Environ
 open Evd
-open Refiner
 
 let refining = Proof_global.there_are_pending_proofs
 let check_no_pending_proofs = Proof_global.check_no_pending_proof
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index c3d0c9053..fea1b701e 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -7,14 +7,10 @@
 (************************************************************************)
 
 open Loc
-open Pp
 open Names
 open Term
-open Context
 open Environ
 open Decl_kinds
-open Tacmach
-open Tacexpr
 
 (** Several proofs can be opened simultaneously but at most one is
    focused at some time. The following functions work by side-effect
diff --git a/proofs/proof.mli b/proofs/proof.mli
index c535fa914..ac922ac50 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -29,8 +29,6 @@
      [give_up] was run and solve the goal there.
 *)
 
-open Term
-
 (* Type of a proof. *)
 type proof
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index bbe8ad531..f5431daaa 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -17,7 +17,6 @@
 open Util
 open Pp
 open Names
-open Util
 
 (*** Proof Modes ***)
 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 4394aeff1..3ee7c87f7 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -14,7 +14,6 @@ open Context
 open Tacexpr
 open Glob_term
 open Nametab
-open Pattern
 open Misctypes
 (*i*)
 
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 4abd6f776..85ecfdd8a 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -6,18 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Environ
 open Evd
 open Names
-open Libnames
 open Term
 open Context
-open Pp
 open Tacexpr
 open Glob_term
-open Genarg
 open Nametab
-open Pattern
 open Misctypes
 
 (** This module defines the structure of proof tree and the tactic type. So, it
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index 31affc280..755497615 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -8,11 +8,9 @@
 
 open Names
 open Term
-open Closure
 open Pattern
 open Genredexpr
 open Reductionops
-open Termops
 open Locus
 
 type red_expr =
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 8fc9e9e17..db2c081d1 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -6,12 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open Context
 open Evd
 open Proof_type
-open Tacexpr
-open Logic
 
 (** The refiner (handles primitive rules and high-level tactics). *)
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index de73f7720..9a03df041 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
 open Util
 open Names
 open Namegen
@@ -205,7 +204,6 @@ let pr_glls glls =
 
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New = struct
-  open Proofview.Notations
 
   let pf_apply f gl =
     f (Proofview.Goal.env gl) (Proofview.Goal.sigma gl)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 48c4f8d48..10f6be1d5 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -11,12 +11,8 @@ open Term
 open Context
 open Environ
 open Evd
-open Reduction
 open Proof_type
-open Refiner
 open Redexpr
-open Tacexpr
-open Glob_term
 open Pattern
 open Locus
 open Misctypes
@@ -134,8 +130,6 @@ val pr_glls   : goal list sigma -> Pp.std_ppcmds
 
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New : sig
-  open Proofview
-
   val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a
   val pf_global : identifier -> Proofview.Goal.t -> constr
   val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 1ae1a3905..bf8507360 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -8,8 +8,6 @@
 
 open Environ
 open Pattern
-open Evd
-open Proof_type
 open Names
 open Tacexpr
 open Term