Merge pull request #705 from FissoreD/warning-unused-open

remove unused module open
LPCIC · Oct 25, 2024 · 59e8757 · 59e8757
2 parents c7fcee1 + dc0ec95
commit 59e8757
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 7 deletions.
diff --git 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
@@ -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