1 files changed, 0 insertions, 6 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 6329a62b9..50410ad82 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -9,23 +9,17 @@
 open Pp
 open Errors
 open Util
-open Univ
 open Names
 open Term
-open Declarations
-open Inductive
 open Inductiveops
 open Environ
-open Sign
 open Glob_term
 open Glob_ops
-open Nameops
 open Termops
 open Namegen
 open Libnames
 open Globnames
 open Nametab
-open Evd
 open Mod_subst
 open Misctypes
 open Decl_kinds