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

6 files changed, 0 insertions, 17 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 4b6bf39be..b6b7e5833 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -7,11 +7,8 @@
 (************************************************************************)
 
 open Pp
-open Errors
 open Util
 open Names
-open Term
-open Declarations
 open Namegen
 open Nameops
 open Libnames
@@ -19,8 +16,6 @@ open Globnames
 open Table
 open Miniml
 open Mlutil
-open Modutil
-open Mod_subst
 
 let string_of_id id =
   let s = Names.string_of_id id in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index ab0e480f9..0556f6d77 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 (*i*)
-open Errors
 open Util
 open Names
 open Term
@@ -20,9 +19,7 @@ open Termops
 open Inductiveops
 open Recordops
 open Namegen
-open Summary
 open Globnames
-open Nametab
 open Miniml
 open Table
 open Mlutil
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index a8c9375b1..3b89386d4 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -7,13 +7,10 @@
 (************************************************************************)
 
 (*i*)
-open Pp
-open Errors
 open Util
 open Names
 open Libnames
 open Globnames
-open Nametab
 open Table
 open Miniml
 (*i*)
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index d2e8e4951..1211bbf17 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -7,15 +7,12 @@
 (************************************************************************)
 
 open Names
-open Declarations
-open Environ
 open Globnames
 open Errors
 open Util
 open Miniml
 open Table
 open Mlutil
-open Mod_subst
 
 (*S Functions upon ML modules. *)
 
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 067c41705..34ae1f9ad 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -19,7 +19,6 @@ open Miniml
 open Mlutil
 open Modutil
 open Common
-open Declarations
 
 
 (*s Some utility functions. *)
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 27529258b..ec338b1db 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -12,8 +12,6 @@ open Pp
 open Errors
 open Util
 open Names
-open Nameops
-open Libnames
 open Miniml
 open Mlutil
 open Table