Remove unused [open] statements

5 files changed, 0 insertions, 5 deletions

diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 7ddc84d015..61752aa339 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -1,5 +1,4 @@
 open Names
-open Term
 
 val prove_princ_for_struct :
   Evd.evar_map ref ->
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 0dccd25d75..b5eacee818 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -8,7 +8,6 @@
 (*i camlp4deps: "grammar/grammar.cma" i*)
 open Ltac_plugin
 open Util
-open Term
 open Pp
 open Constrexpr
 open Indfun_common
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 7b0d7d27d7..c6f5c27458 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -508,7 +508,6 @@ let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) =
        (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
 
 let decompose_lam_n sigma n =
-  let open EConstr in
   if n < 0 then CErrors.error "decompose_lam_n: integer parameter must be positive";
   let rec lamdec_rec l n c =
     if Int.equal n 0 then l,c
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 94ec0a898a..29472cdef3 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Ltac_plugin
-open Tacexpr
 open Declarations
 open CErrors
 open Util
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index f1ca575856..0af0898a0a 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -19,7 +19,6 @@ open Pp
 open Names
 open Term
 open Vars
-open Termops
 open Declarations
 open Glob_term
 open Glob_termops