Remove unused [open] statements

24 files changed, 0 insertions, 42 deletions

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 62f811546d..2b624b9833 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -17,7 +17,6 @@ open Tacmach.New
 open Tactics
 open Tacticals.New
 open Proofview.Notations
-open Termops
 open Reductionops
 open Formula
 open Sequent
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
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 5d3f6df03d..bc9c300e23 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -9,7 +9,6 @@
 open Util
 open Names
 open Term
-open EConstr
 open CErrors
 open Evar_refiner
 open Tacmach
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 35cfe8b542..21419d1f92 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -21,7 +21,6 @@ open Tacexpr
 open Glob_ops
 open CErrors
 open Util
-open Evd
 open Termops
 open Equality
 open Misctypes
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index dfa8331ff2..50e8255a67 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -16,7 +16,6 @@ open Pcoq.Constr
 open Pltac
 open Hints
 open Tacexpr
-open Proofview.Notations
 open Names
 
 DECLARE PLUGIN "g_auto"
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index ff5e7d5ff2..23ce368eea 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -8,9 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open Misctypes
 open Class_tactics
-open Pltac
 open Stdarg
 open Tacarg
 open Names
@@ -95,7 +93,6 @@ END
 (** TODO: DEPRECATE *)
 (* A progress test that allows to see if the evars have changed *)
 open Term
-open Proofview.Goal
 open Proofview.Notations
 
 let rec eq_constr_mod_evars sigma x y =
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 1d21118ae8..7e979d269d 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Pcoq
 
 (* Main entry for extensions *)
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 7a20838a27..6683d753bc 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -14,7 +14,6 @@ open Constrexpr
 open Tacexpr
 open Misctypes
 open Evd
-open Proof_type
 open Tacinterp
 
 (** TODO: document and clean me! *)
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 9c4ac52657..4a44f86d92 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -8,7 +8,6 @@
 
 open Util
 open Names
-open Term
 open EConstr
 open Misctypes
 open Pattern
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index ef1d69d35b..32750383b8 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -15,7 +15,6 @@ open Genarg
 open Extend
 open Pcoq
 open Egramml
-open Egramcoq
 open Vernacexpr
 open Libnames
 open Nameops
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 94e14223aa..d1e2a7bbe6 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Genarg
 open Names
 open Tacexpr
 open Geninterp
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index fcdf7bb2cd..b8c021f188 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -25,7 +25,6 @@ open Refiner
 open Tacmach.New
 open Tactic_debug
 open Constrexpr
-open Term
 open Termops
 open Tacexpr
 open Genarg
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 1e5f6bd42b..494f36a95a 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Tactic_debug
-open Term
 open EConstr
 open Tacexpr
 open Genarg
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index 7745d9b7b6..0b4d35a22a 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -10,7 +10,6 @@ open Environ
 open Pattern
 open Names
 open Tacexpr
-open Term
 open EConstr
 open Evd
 
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index eb26c5431d..a36607ec38 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -331,7 +331,6 @@ module M =
 struct
 
   open Coqlib
-  open Term
   open Constr
   open EConstr
 
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index 41f2edfcf1..a120d4efb2 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -196,8 +196,6 @@ module Hashpol = Hashtbl.Make(
 
 (* A pretty printer for polynomials, with Maple-like syntax. *)
 
-open Format
-
 let getvar lv i =
   try (List.nth lv i)
   with Failure _ -> (List.fold_left (fun r x -> r^" "^x) "lv= " lv)
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 6e072e8317..d59ffee546 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -19,7 +19,6 @@ open Environ
 open Libnames
 open Globnames
 open Glob_term
-open Tacticals
 open Tacexpr
 open Coqlib
 open Mod_subst
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
index 4367d021c0..d9d32c681d 100644
--- a/plugins/setoid_ring/newring.mli
+++ b/plugins/setoid_ring/newring.mli
@@ -7,13 +7,10 @@
 (************************************************************************)
 
 open Names
-open Constr
 open EConstr
 open Libnames
 open Globnames
 open Constrexpr
-open Tacexpr
-open Proof_type
 open Newring_ast
 
 val protect_tac_in : string -> Id.t -> unit Proofview.tactic
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index f146fbb118..72c70750c9 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -21,30 +21,21 @@ open Pp
 open Pcoq
 open Genarg
 open Stdarg
-open Tacarg
 open Term
 open Vars
-open Topconstr
 open Libnames
 open Tactics
 open Tacticals
 open Termops
-open Namegen
 open Recordops
 open Tacmach
-open Coqlib
 open Glob_term
 open Util
 open Evd
-open Extend
-open Goptions
 open Tacexpr
-open Proofview.Notations
 open Tacinterp
 open Pretyping
 open Constr
-open Pltac
-open Extraargs
 open Ppconstr
 open Printer
 
@@ -54,14 +45,9 @@ open Decl_kinds
 open Evar_kinds
 open Constrexpr
 open Constrexpr_ops
-open Notation_term
-open Notation_ops
-open Locus
-open Locusops
 
 DECLARE PLUGIN "ssrmatching_plugin"
 
-type loc = Loc.t
 let dummy_loc = Loc.ghost
 let errorstrm = CErrors.user_err ~hdr:"ssrmatching"
 let loc_error loc msg = CErrors.user_err ~loc ~hdr:msg (str msg)
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 1f984b1609..638b4e254e 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -4,7 +4,6 @@
 open Genarg
 open Tacexpr
 open Environ
-open Tacmach
 open Evd
 open Proof_type
 open Term