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

20 files changed, 0 insertions, 76 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index e8abd8e17d..59cc3afd83 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -11,20 +11,12 @@
 
 open Tacmach
 open Errors
-open Util
-open Flags
-open Decl_kinds
 open Pp
-open Entries
 open Termops
 open Declarations
-open Declare
 open Term
 open Names
 open Globnames
-open Goptions
-open Mod_subst
-open Indrec
 open Inductiveops
 open Tactics
 open Tacticals
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 4c991056e8..2338e7f390 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -12,7 +12,6 @@ open Printer
 open Names
 open Term
 open Evd
-open Sign
 open Globnames
 (*i*)
 
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 74e4701c0f..d1e379cca2 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -8,7 +8,6 @@
 
 open Pp
 open Errors
-open Util
 open Indtypes
 open Type_errors
 open Pretype_errors
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 78b7123014..dfb74b9e9e 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -7,25 +7,17 @@
 (************************************************************************)
 
 open Errors
-open Util
 open Pp
 open Names
-open Nameops
 open Term
 open Termops
-open Inductive
-open Declarations
 open Entries
 open Environ
-open Inductive
-open Lib
 open Classops
 open Declare
-open Libnames
 open Globnames
 open Nametab
 open Decl_kinds
-open Safe_typing
 
 let strength_min l = if List.mem Local l then Local else Global
 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index b3f9d48726..c4c017577d 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -8,23 +8,17 @@
 
 (*i*)
 open Names
-open Decl_kinds
 open Term
-open Sign
-open Entries
 open Evd
 open Environ
 open Nametab
-open Mod_subst
 open Errors
-open Pp
 open Util
 open Typeclasses_errors
 open Typeclasses
 open Libnames
 open Globnames
 open Constrintern
-open Glob_term
 open Constrexpr
 (*i*)
 
@@ -73,7 +67,6 @@ type binder_list = (identifier Loc.located * bool * constr_expr) list
 
 (* Declare everything in the parameters as implicit, and the class instance as well *)
 
-open Topconstr
 
 let type_ctx_instance evars env ctx inst subst =
   let rec aux (subst, instctx) l = function
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index eac009984c..718e65b50a 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 open Pp
-open System
-open Toplevel
 
 let (/) = Filename.concat
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index f06edd3168..df155eebb7 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -13,9 +13,7 @@ open System
 open Flags
 open Names
 open Libnames
-open Nameops
 open States
-open Toplevel
 open Coqinit
 
 let () = at_exit flush_all
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index b4648246ac..3cdeb0be90 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -7,15 +7,12 @@
 (************************************************************************)
 
 open Pp
-open Errors
 open Util
-open Flags
 open Names
 open Nameops
 open Namegen
 open Term
 open Termops
-open Inductive
 open Indtypes
 open Sign
 open Environ
@@ -23,11 +20,9 @@ open Pretype_errors
 open Type_errors
 open Typeclasses_errors
 open Indrec
-open Reduction
 open Cases
 open Logic
 open Printer
-open Glob_term
 open Evd
 
 let pr_lconstr c = quote (pr_lconstr c)
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 13b4d13fe9..a7bc895c9a 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -7,12 +7,9 @@
 (************************************************************************)
 
 open Vernacexpr
-open Names
 open Errors
-open Util
 open Pp
 open Printer
-open Namegen
 
 (** Ide_slave : an implementation of [Interface], i.e. mainly an interp
     function and a rewind function. This specialized loop is triggered
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index bb60fed736..b99f83e5cd 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -15,7 +15,6 @@
    declaring new schemes *)
 
 open Pp
-open Flags
 open Errors
 open Util
 open Names
@@ -31,10 +30,7 @@ open Globnames
 open Goptions
 open Nameops
 open Termops
-open Typeops
-open Inductiveops
 open Pretyping
-open Topconstr
 open Nametab
 open Smartlocate
 open Vernacexpr
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 5680f993ee..0c9cf877d0 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -26,7 +26,6 @@ open Declare
 open Pretyping
 open Termops
 open Namegen
-open Evd
 open Evarutil
 open Reductionops
 open Constrexpr
diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml
index d85695d504..0866db092e 100644
--- a/toplevel/libtypes.ml
+++ b/toplevel/libtypes.ml
@@ -10,7 +10,6 @@ open Term
 open Summary
 open Libobject
 open Globnames
-open Names
 (*
  * Module construction
  *)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 77949a1265..4eebfc8f73 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -19,11 +19,9 @@ open Notation_ops
 open Ppextend
 open Extend
 open Libobject
-open Summary
 open Constrintern
 open Vernacexpr
 open Pcoq
-open Glob_term
 open Libnames
 open Tok
 open Lexer
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 6338fa9e43..2a0f3c1671 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -1,18 +1,9 @@
 open Printf
-open Pp
-open Environ
-open Term
-open Names
 open Globnames
-open Summary
 open Libobject
 open Entries
 open Decl_kinds
-open Errors
-open Util
-open Evd
 open Declare
-open Proof_type
 
 (**
    - Get types of existentials ;
@@ -537,7 +528,6 @@ let declare_definition prg =
       (fun local gr -> prg.prg_hook local gr; gr)
 
 open Pp
-open Ppconstr
 
 let rec lam_index n t acc =
   match kind_of_term t with
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 88ff5e6461..978329e137 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -17,13 +17,8 @@ open Environ
 open Declarations
 open Entries
 open Declare
-open Nametab
 open Constrintern
-open Command
-open Inductive
-open Safe_typing
 open Decl_kinds
-open Indtypes
 open Type_errors
 open Constrexpr
 open Constrexpr_ops
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 3ab4feb5e8..81fdf84aa2 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -10,12 +10,9 @@ open Pp
 open Errors
 open Util
 open Names
-open Nameops
 open Term
-open Glob_term
 open Declarations
 open Libobject
-open Declare
 open Environ
 open Pattern
 open Matching
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index fe6dbe642b..ace83cf64d 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -8,9 +8,7 @@
 
 open Pp
 open Errors
-open Util
 open Flags
-open Cerrors
 open Vernac
 open Pcoq
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index b897a6d919..a494a10cc1 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -10,7 +10,6 @@
 
 open Pp
 open Errors
-open Util
 open Flags
 open System
 open Vernacexpr
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c30c6c0c17..18cef702c8 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -13,7 +13,6 @@ open Errors
 open Util
 open Flags
 open Names
-open Entries
 open Nameops
 open Term
 open Pfedit
@@ -26,13 +25,10 @@ open Command
 open Goptions
 open Libnames
 open Globnames
-open Nametab
 open Vernacexpr
 open Decl_kinds
 open Constrexpr
-open Pretyping
 open Redexpr
-open Syntax_def
 open Lemmas
 open Declaremods
 open Misctypes
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 242667f3a3..dca47f7146 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -8,12 +8,6 @@
 
 open Pp
 open Errors
-open Util
-open Names
-open Libnames
-open Himsg
-open Proof_type
-open Tacinterp
 
 let disable_drop e =
   if e <> Drop then e