aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/firstorder/instances.ml1
-rw-r--r--plugins/funind/functional_principles_proofs.mli1
-rw-r--r--plugins/funind/g_indfun.ml41
-rw-r--r--plugins/funind/indfun_common.ml1
-rw-r--r--plugins/funind/invfun.ml1
-rw-r--r--plugins/funind/merge.ml1
-rw-r--r--plugins/ltac/evar_tactics.ml1
-rw-r--r--plugins/ltac/extratactics.ml41
-rw-r--r--plugins/ltac/g_auto.ml41
-rw-r--r--plugins/ltac/g_class.ml43
-rw-r--r--plugins/ltac/pltac.ml1
-rw-r--r--plugins/ltac/rewrite.mli1
-rw-r--r--plugins/ltac/taccoerce.mli1
-rw-r--r--plugins/ltac/tacentries.ml1
-rw-r--r--plugins/ltac/tacenv.mli1
-rw-r--r--plugins/ltac/tacinterp.ml1
-rw-r--r--plugins/ltac/tacinterp.mli1
-rw-r--r--plugins/ltac/tactic_debug.mli1
-rw-r--r--plugins/micromega/coq_micromega.ml1
-rw-r--r--plugins/nsatz/ideal.ml2
-rw-r--r--plugins/setoid_ring/newring.ml1
-rw-r--r--plugins/setoid_ring/newring.mli3
-rw-r--r--plugins/ssrmatching/ssrmatching.ml414
-rw-r--r--plugins/ssrmatching/ssrmatching.mli1
24 files changed, 0 insertions, 42 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 62f811546..2b624b983 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 7ddc84d01..61752aa33 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 0dccd25d7..b5eacee81 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 7b0d7d27d..c6f5c2745 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 94ec0a898..29472cdef 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 f1ca57585..0af0898a0 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 5d3f6df03..bc9c300e2 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 35cfe8b54..21419d1f9 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 dfa8331ff..50e8255a6 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 ff5e7d5ff..23ce368ee 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 1d21118ae..7e979d269 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 7a20838a2..6683d753b 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 9c4ac5265..4a44f86d9 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 ef1d69d35..32750383b 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 94e14223a..d1e2a7bbe 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 fcdf7bb2c..b8c021f18 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 1e5f6bd42..494f36a95 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 7745d9b7b..0b4d35a22 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 eb26c5431..a36607ec3 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 41f2edfcf..a120d4efb 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 6e072e831..d59ffee54 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 4367d021c..d9d32c681 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 f146fbb11..72c70750c 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 1f984b160..638b4e254 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 16:31:52 +0000