1 files changed, 0 insertions, 5 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index ae4e3b2f8..9791598fd 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -10,21 +10,16 @@ open Pp
 open Errors
 open Util
 open Names
-open Nameops
 open Term
 open Libnames
 open Globnames
 open Termops
 open Namegen
-open Declarations
-open Inductive
 open Libobject
 open Environ
 open Closure
 open Reductionops
 open Cbv
-open Glob_term
-open Pattern
 open Patternops
 open Matching
 open Locus