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, 71 deletions

diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 9809d4d099..b5bb27da96 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
 open Term
 open Context
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 58265208b7..886e00e835 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -18,7 +18,6 @@ open Environ
 open Libobject
 open Term
 open Termops
-open Decl_kinds
 open Mod_subst
 
 (* usage qque peu general: utilise aussi dans record *)
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index d0c7793ae6..7bde9e910e 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -7,11 +7,9 @@
 (************************************************************************)
 
 open Names
-open Decl_kinds
 open Term
 open Evd
 open Environ
-open Nametab
 open Mod_subst
 
 (** {6 This is the type of class kinds } *)
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index f5c548cc43..c1b114c913 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -6,13 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Evd
 open Names
 open Term
-open Context
 open Environ
-open Evarutil
 open Glob_term
 
 (** {6 Coercions. } *)
diff --git a/pretyping/constrMatching.mli b/pretyping/constrMatching.mli
index b82f115251..19cf348775 100644
--- a/pretyping/constrMatching.mli
+++ b/pretyping/constrMatching.mli
@@ -12,7 +12,6 @@ open Names
 open Term
 open Environ
 open Pattern
-open Termops
 
 (** [PatternMatchingFailure] is the exception raised when pattern
   matching fails *)
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 8a10b7ed5e..2cca25fd25 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Pp
 open Names
 open Term
 open Context
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 89993189f1..3a8e4fab5a 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -8,9 +8,7 @@
 
 open Names
 open Term
-open Context
 open Environ
-open Termops
 open Reductionops
 open Evd
 open Locus
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 20a4a3f9e3..bdc4bc0ae1 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Util
 open Errors
 open Names
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index f4636cdaa4..49ce29fdfb 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -20,7 +20,6 @@ open Environ
 open Evd
 open Reductionops
 open Pretype_errors
-open Retyping
 
 (****************************************************)
 (* Expanding/testing/exposing existential variables *)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 7e1f7df88b..f41f1ec862 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -6,15 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
-open Util
 open Names
-open Glob_term
 open Term
 open Context
 open Evd
 open Environ
-open Reductionops
 
 (** {5 This modules provides useful functions for unification modulo evars } *)
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 2b0e9ca684..8f423c7881 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -8,14 +8,11 @@
 
 open Util
 open Loc
-open Pp
 open Names
 open Term
 open Context
 open Environ
-open Libnames
 open Mod_subst
-open Termops
 
 (** {5 Existential variables and unification states}
 
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 1785c87be8..9e0aac909f 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -6,15 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
-open Context
-open Term
-open Libnames
-open Nametab
-open Decl_kinds
-open Misctypes
-open Locus
 open Glob_term
 
 (** Equalities *)
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index 610a7bf39b..6bcfac20ed 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -8,8 +8,6 @@
 
 open Names
 open Term
-open Declarations
-open Inductiveops
 open Environ
 open Evd
 
diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli
index ddf615033e..a086a6f58f 100644
--- a/pretyping/locusops.mli
+++ b/pretyping/locusops.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Misctypes
 open Locus
 
 (** Utilities on occurrences *)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index cc2054d100..af7a99320b 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -16,10 +16,7 @@ open Declarations
 open Names
 open Inductive
 open Util
-open Unix
 open Nativecode
-open Inductiveops
-open Closure
 open Nativevalues
 open Nativelambda
 
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index a589846b9a..8f65ddb2f6 100644
--- a/pretyping/nativenorm.mli
+++ b/pretyping/nativenorm.mli
@@ -5,10 +5,8 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-open Names
 open Term
 open Environ
-open Reduction
 open Evd
 open Nativelambda
 
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 5cc4049ba2..cfe71510a1 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -6,13 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
-open Names
 open Context
 open Term
-open Environ
 open Globnames
-open Nametab
 open Glob_term
 open Mod_subst
 open Misctypes
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 404f5b4012..8ffd53055e 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -9,9 +9,6 @@
 open Util
 open Names
 open Term
-open Vars
-open Termops
-open Namegen
 open Environ
 open Type_errors
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 996b751465..8e98f63076 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -6,13 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
 open Term
-open Context
 open Environ
-open Glob_term
-open Inductiveops
 open Type_errors
 
 (** {6 The type of errors raised by the pretyper } *)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 6994723ac6..ec8aae1403 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -13,7 +13,6 @@
    implicit arguments. *)
 
 open Names
-open Context
 open Term
 open Environ
 open Evd
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 88199c4349..42663c0144 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -7,10 +7,8 @@
 (************************************************************************)
 
 open Names
-open Nametab
 open Term
 open Globnames
-open Libobject
 
 (** Operations concerning records and canonical structures *)
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index aff65d53a3..5ba0d74eca 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -12,7 +12,6 @@ open Context
 open Univ
 open Evd
 open Environ
-open Closure
 
 (** Reduction Functions. *)
 
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 963d61ca2d..bb3ffa4116 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Term
 open Evd
 open Environ
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 4b03c935f5..dd7542fc7f 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -16,7 +16,6 @@ open Libnames
 open Globnames
 open Termops
 open Namegen
-open Libobject
 open Environ
 open Closure
 open Reductionops
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index be92be51a0..34aca3e332 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -11,9 +11,6 @@ open Term
 open Environ
 open Evd
 open Reductionops
-open Closure
-open Glob_term
-open Termops
 open Pattern
 open Globnames
 open Locus
diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli
index 2560ae080a..7825ebdf1a 100644
--- a/pretyping/term_dnet.mli
+++ b/pretyping/term_dnet.mli
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 open Term
-open Context
-open Libnames
 open Mod_subst
 
 (** Dnets on constr terms.
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index d9213fc133..d0d3fd767e 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
 open Pp
 open Names
 open Term
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 0fe22bcce3..c362935253 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -8,14 +8,10 @@
 
 open Names
 open Globnames
-open Decl_kinds
 open Term
 open Context
 open Evd
 open Environ
-open Nametab
-open Mod_subst
-open Topconstr
 
 type direction = Forward | Backward
 
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 94bbfce00e..b3cfb37fa0 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -8,15 +8,11 @@
 
 open Loc
 open Names
-open Decl_kinds
 open Term
 open Context
 open Evd
 open Environ
-open Nametab
-open Mod_subst
 open Constrexpr
-open Pp
 open Globnames
 
 type contexts = Parameters | Properties
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index bbcc5727b4..0cd9099e35 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -14,7 +14,6 @@ open Vars
 open Environ
 open Reductionops
 open Type_errors
-open Pretype_errors
 open Inductive
 open Inductiveops
 open Typeops
diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli
index ca370b559d..9731e3590b 100644
--- a/pretyping/vnorm.mli
+++ b/pretyping/vnorm.mli
@@ -6,10 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Term
 open Environ
-open Reduction
 
 (** {6 Reduction functions } *)
 val cbv_vm : env -> constr -> types -> constr