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

13 files changed, 0 insertions, 35 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 65ff2a53e..950edc5a3 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -9,12 +9,8 @@
 open Pp
 open Util
 open Names
-open Nameops
 open Libnames
-open Misctypes
-open Term
 open Glob_term
-open Mod_subst
 open Constrexpr
 open Decl_kinds
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index a59345938..272845d07 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -10,21 +10,15 @@
 open Pp
 open Errors
 open Util
-open Univ
 open Names
 open Nameops
 open Term
 open Termops
-open Namegen
-open Inductive
-open Sign
-open Environ
 open Libnames
 open Globnames
 open Impargs
 open Constrexpr
 open Constrexpr_ops
-open Notation_term
 open Notation_ops
 open Topconstr
 open Glob_term
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d83780fb4..86998c210 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -18,7 +18,6 @@ open Globnames
 open Impargs
 open Glob_term
 open Glob_ops
-open Pattern
 open Patternops
 open Pretyping
 open Cases
@@ -1766,7 +1765,6 @@ let interp_binder_evars evdref env na t =
   understand_tcc_evars evdref env IsType t'
 
 open Environ
-open Term
 
 let my_intern_constr sigma env lvar acc c =
   internalize sigma env acc false lvar c
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index d7c415306..94cb91749 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -13,7 +13,6 @@ open Names
 open Term
 open Libnames
 open Globnames
-open Pattern
 open Nametab
 open Smartlocate
 
diff --git a/interp/genarg.ml b/interp/genarg.ml
index cfa968363..9e3528cf4 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Glob_term
 open Constrexpr
 open Misctypes
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 47d4c4af5..3057cef34 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -9,12 +9,6 @@
 (*i*)
 open Names
 open Decl_kinds
-open Term
-open Sign
-open Evd
-open Environ
-open Nametab
-open Mod_subst
 open Errors
 open Util
 open Glob_term
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 7974c3709..1e7d84c96 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Errors
-open Util
 open Names
 open Entries
 open Libnames
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index ae851d8ba..bd3ba4274 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -15,9 +15,7 @@ open Globnames
 open Misctypes
 open Glob_term
 open Glob_ops
-open Term
 open Mod_subst
-open Constrexpr
 open Notation_term
 open Decl_kinds
 
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 50379b67e..562764612 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Names
 
 (*s Pretty-print. *)
 
diff --git a/interp/reserve.ml b/interp/reserve.ml
index b271dab69..259ffa171 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -13,7 +13,6 @@ open Util
 open Pp
 open Names
 open Nameops
-open Summary
 open Libobject
 open Lib
 open Notation_term
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 1a59f8ed6..adf611b56 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -14,8 +14,6 @@
 (* *)
 open Pp
 open Errors
-open Util
-open Names
 open Libnames
 open Globnames
 open Misctypes
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 202a3d770..830778307 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Errors
-open Util
 open Pp
 open Names
 open Libnames
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index f63b46946..e717e1747 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -13,15 +13,9 @@ open Util
 open Names
 open Nameops
 open Libnames
-open Glob_term
-open Glob_ops
-open Term
-open Mod_subst
 open Misctypes
-open Decl_kinds
 open Constrexpr
 open Constrexpr_ops
-open Notation_term
 (*i*)