6 files changed, 0 insertions, 17 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 4b6bf39be1..b6b7e58338 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 ab0e480f9a..0556f6d77f 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 a8c9375b18..3b89386d40 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 d2e8e4951d..1211bbf173 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 067c417056..34ae1f9ad8 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 27529258ba..ec338b1dbf 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