7 files changed, 1 insertions, 7 deletions
diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index 7548c338a0..982fb47ad2 100644
--- a/plugins/decl_mode/decl_expr.mli
+++ b/plugins/decl_mode/decl_expr.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Pp
 open Tacexpr
 
 type 'it statement =
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index a722daca52..505d7dba5c 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -11,7 +11,6 @@ open Util
 open Names
 open Constrexpr
 open Tacintern
-open Tacinterp
 open Decl_expr
 open Decl_mode
 open Pretyping
diff --git a/plugins/decl_mode/decl_interp.mli b/plugins/decl_mode/decl_interp.mli
index 88fb9653ae..6fbf5d25c9 100644
--- a/plugins/decl_mode/decl_interp.mli
+++ b/plugins/decl_mode/decl_interp.mli
@@ -8,7 +8,6 @@
 
 open Tacintern
 open Decl_expr
-open Mod_subst
 
 
 val intern_proof_instr : glob_sign -> raw_proof_instr -> glob_proof_instr
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
index 8e691f508f..1ed1abaf75 100644
--- a/plugins/decl_mode/decl_mode.mli
+++ b/plugins/decl_mode/decl_mode.mli
@@ -9,7 +9,6 @@
 open Names
 open Term
 open Evd
-open Tacmach
 
 val set_daimon_flag : unit -> unit
 val clear_daimon_flag : unit -> unit
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 45ffb450f6..de57330ecf 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -13,7 +13,6 @@ open Evd
 
 open Tacmach
 open Tacintern
-open Tacinterp
 open Decl_expr
 open Decl_mode
 open Decl_interp
diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli
index d78ca84d12..458318264e 100644
--- a/plugins/decl_mode/decl_proof_instr.mli
+++ b/plugins/decl_mode/decl_proof_instr.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Refiner
 open Names
 open Term
 open Tacmach
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index fe75d17f6a..7c9ef3c2a8 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -11,11 +11,11 @@
 open Util
 open Compat
 open Pp
-open Tok
 open Decl_expr
 open Names
 open Pcoq
 open Vernacexpr
+open Tok (* necessary for camlp4 *)
 
 open Pcoq.Constr
 open Pcoq.Tactic