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

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 7e281e0565..f9eafd3ec3 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -9,18 +9,9 @@
 (*i*)
 open Names
 open Globnames
-open Decl_kinds
 open Term
-open Sign
-open Evd
 open Environ
-open Nametab
-open Mod_subst
-open Errors
-open Util
-open Pp
 open Libobject
-open Nameops
 (*i*)
 
 let empty_name_table = (Refmap.empty : name list list Refmap.t)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 5c3e8fe922..163675dfb3 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Errors
 open Util
 open Names
@@ -17,9 +16,7 @@ open Namegen
 open Declarations
 open Inductiveops
 open Environ
-open Sign
 open Reductionops
-open Typeops
 open Type_errors
 open Glob_term
 open Glob_ops
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 6c594ef047..fd88049b24 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -6,15 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
 open Util
-open Pp
 open Term
 open Names
-open Environ
-open Univ
-open Evd
-open Conv_oracle
 open Closure
 open Esubst
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 765cd4ed18..a1b7e5e9dd 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -16,10 +16,8 @@ open Globnames
 open Nametab
 open Environ
 open Libobject
-open Library
 open Term
 open Termops
-open Glob_term
 open Decl_kinds
 open Mod_subst
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index bd23501a83..0b48654b69 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -14,7 +14,6 @@
    Corbineau, Feb 2008 *)
 (* Turned into an abstract compilation unit by Matthieu Sozeau, March 2006 *)
 
-open Pp
 open Errors
 open Util
 open Names
@@ -24,10 +23,8 @@ open Environ
 open Typeops
 open Pretype_errors
 open Classops
-open Recordops
 open Evarutil
 open Evarconv
-open Retyping
 open Evd
 open Termops
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 6329a62b9a..50410ad825 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -9,23 +9,17 @@
 open Pp
 open Errors
 open Util
-open Univ
 open Names
 open Term
-open Declarations
-open Inductive
 open Inductiveops
 open Environ
-open Sign
 open Glob_term
 open Glob_ops
-open Nameops
 open Termops
 open Namegen
 open Libnames
 open Globnames
 open Nametab
-open Evd
 open Mod_subst
 open Misctypes
 open Decl_kinds
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 662cd83046..0740068721 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Errors
 open Util
 open Names
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 90492d50c7..3256afd28b 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -10,11 +10,9 @@ open Errors
 open Util
 open Pp
 open Names
-open Univ
 open Term
 open Termops
 open Namegen
-open Sign
 open Pre_env
 open Environ
 open Evd
@@ -1894,7 +1892,6 @@ let check_evars env initial_sigma sigma c =
       | _ -> iter_constr proc_rec c
   in proc_rec c
 
-open Glob_term
 
 (****************************************)
 (* Operations on value/type constraints *)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 66ebb7f783..a73a74f457 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -13,9 +13,7 @@ open Names
 open Nameops
 open Term
 open Termops
-open Sign
 open Environ
-open Libnames
 open Globnames
 open Mod_subst
 
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index e856570837..a090094aaa 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -6,17 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Pp
 open Util
 open Names
-open Sign
-open Term
 open Globnames
-open Nametab
-open Decl_kinds
 open Misctypes
-open Locus
 open Glob_term
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 7ccd62776d..025f7f6687 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -20,16 +20,11 @@ open Nameops
 open Term
 open Namegen
 open Declarations
-open Entries
 open Inductive
 open Inductiveops
 open Environ
 open Reductionops
-open Typeops
-open Type_errors
-open Safe_typing
 open Nametab
-open Sign
 
 type dep_flag = bool
 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 1c7302fe0f..19126f01bc 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -13,7 +13,6 @@ open Univ
 open Term
 open Termops
 open Namegen
-open Sign
 open Declarations
 open Environ
 open Reductionops
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index c9f60df61e..161243587c 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
-open Misctypes
 open Locus
 
 (** Utilities on occurrences *)
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index a4c16b7242..bc9c832ae7 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -16,9 +16,6 @@ open Nameops
 open Termops
 open Reductionops
 open Term
-open Glob_term
-open Sign
-open Environ
 open Pattern
 open Patternops
 open Misctypes
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index fc84c8efa4..9d57773589 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -12,7 +12,6 @@
 (* This file is about generating new or fresh names and dealing with
    alpha-renaming *)
 
-open Errors
 open Util
 open Names
 open Term
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 68382f15a2..c3b03e209d 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -14,8 +14,6 @@ open Nameops
 open Term
 open Glob_term
 open Glob_ops
-open Environ
-open Nametab
 open Pp
 open Mod_subst
 open Misctypes
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 57bb8512ef..d9a050c083 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -6,17 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
 open Names
-open Sign
 open Term
 open Termops
 open Namegen
 open Environ
 open Type_errors
-open Glob_term
-open Inductiveops
 
 type pretype_error =
   (* Old Case *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index cbaa988442..5113236954 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -33,11 +33,8 @@ open Reductionops
 open Environ
 open Type_errors
 open Typeops
-open Libnames
 open Globnames
 open Nameops
-open Classops
-open Recordops
 open Evarutil
 open Pretype_errors
 open Glob_term
@@ -55,7 +52,6 @@ type pure_open_constr = evar_map * constr
 
 (************************************************************************)
 (* This concerns Cases *)
-open Declarations
 open Inductive
 open Inductiveops
 
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 06c4a1d74a..db821f1762 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -6,22 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Errors
 open Util
 open Names
 open Term
-open Reductionops
-open Environ
-open Typeops
-open Pretype_errors
-open Classops
-open Recordops
-open Evarutil
-open Evarconv
-open Retyping
-open Evd
-open Termops
 
 type message = string
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 4f7d06e393..7c128d245d 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -20,9 +20,7 @@ open Names
 open Globnames
 open Nametab
 open Term
-open Typeops
 open Libobject
-open Library
 open Mod_subst
 open Reductionops
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index bdc6cb72a9..0b5ad7b0bf 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Errors
 open Util
 open Names
@@ -14,10 +13,8 @@ open Term
 open Termops
 open Univ
 open Evd
-open Declarations
 open Environ
 open Closure
-open Esubst
 open Reduction
 
 exception Elimconst
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 22ffcb56e1..1909528c54 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -7,14 +7,12 @@
 (************************************************************************)
 
 open Errors
-open Util
 open Term
 open Inductive
 open Inductiveops
 open Names
 open Reductionops
 open Environ
-open Typeops
 open Declarations
 open Termops
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index ae4e3b2f8c..9791598fd8 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -10,21 +10,16 @@ open Pp
 open Errors
 open Util
 open Names
-open Nameops
 open Term
 open Libnames
 open Globnames
 open Termops
 open Namegen
-open Declarations
-open Inductive
 open Libobject
 open Environ
 open Closure
 open Reductionops
 open Cbv
-open Glob_term
-open Pattern
 open Patternops
 open Matching
 open Locus
diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
index 49c93ffddb..8e56d59a66 100644
--- a/pretyping/term_dnet.ml
+++ b/pretyping/term_dnet.ml
@@ -7,10 +7,8 @@
 (************************************************************************)
 
 (*i*)
-open Errors
 open Util
 open Term
-open Sign
 open Names
 open Globnames
 open Mod_subst
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 9bd539abc3..e4f481e58d 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -12,10 +12,7 @@ open Util
 open Names
 open Nameops
 open Term
-open Sign
 open Environ
-open Libnames
-open Nametab
 open Locus
 
 (* Sorts and sort family *)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 3e91837804..8fd0f768ea 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -14,9 +14,6 @@ open Term
 open Sign
 open Evd
 open Environ
-open Nametab
-open Mod_subst
-open Errors
 open Util
 open Typeclasses_errors
 open Libobject
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 5350ecfcc1..4a0b66a7b6 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -8,16 +8,10 @@
 
 (*i*)
 open Names
-open Decl_kinds
 open Term
-open Sign
 open Evd
 open Environ
-open Nametab
-open Mod_subst
 open Constrexpr
-open Pp
-open Util
 open Globnames
 (*i*)
 
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index ebb30bf35c..df1833f843 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -8,7 +8,6 @@
 
 open Errors
 open Util
-open Names
 open Term
 open Environ
 open Reductionops
@@ -17,7 +16,6 @@ open Pretype_errors
 open Inductive
 open Inductiveops
 open Typeops
-open Evd
 open Arguments_renaming
 
 let meta_type evd mv =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 20446ba00a..7821a5f4f7 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,20 +6,16 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Errors
 open Util
 open Names
-open Nameops
 open Term
 open Termops
 open Namegen
-open Sign
 open Environ
 open Evd
 open Reduction
 open Reductionops
-open Glob_term
 open Evarutil
 open Pretype_errors
 open Retyping