diff --git a/apps/cs/src/coq_elpi_cs_hook.mlg b/apps/cs/src/coq_elpi_cs_hook.mlg
index 7fb485a03..49ff40a60 100644
--- a/apps/cs/src/coq_elpi_cs_hook.mlg
+++ b/apps/cs/src/coq_elpi_cs_hook.mlg
@@ -57,11 +57,6 @@ let elpi_cs_hook program env sigma ((proji, u), params1, c1) (t2, args2) =
 		 | API.Execute.Failure -> None
 		 end
 
-open Elpi
-open Elpi_plugin
-open Coq_elpi_arg_syntax
-open Coq_elpi_vernacular
-
 [%%if coq = "8.20"]
 let adapt_hook f : Evarconv.hook = fun env sigma (s,l,t) x -> f env sigma (s,Some l,t) x
 [%%else]
diff --git a/src/coq_elpi_utils.ml b/src/coq_elpi_utils.ml
index 7f7022377..ad0979090 100644
--- a/src/coq_elpi_utils.ml
+++ b/src/coq_elpi_utils.ml
@@ -256,7 +256,6 @@ let detype_universe sigma u =
   Glob_term.UNamed (List.map (Util.on_fst (detype_level_name sigma)) (Univ.Universe.repr u))
 let detype_sort ku sigma x =
   let open Sorts in
-  let open Glob_term in
   let open Glob_ops in
   match x with
   | SProp -> glob_SProp_sort
@@ -313,7 +312,6 @@ end =
 struct
 open Vars
 open Names
-open EConstr
 open Declarations
 open UVars
 open Constr