1 files changed, 0 insertions, 9 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b181dc534..9f4f0e9ce 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -7,26 +7,17 @@
 (************************************************************************)
 
 open Loc
-open Pp
 open Names
 open Term
 open Context
 open Environ
-open Tacmach
 open Proof_type
-open Reduction
 open Evd
-open Evar_refiner
 open Clenv
 open Redexpr
-open Tacticals
 open Globnames
-open Genarg
 open Tacexpr
-open Nametab
-open Glob_term
 open Pattern
-open Termops
 open Unification
 open Misctypes
 open Locus