aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml35
-rw-r--r--tactics/autorewrite.ml6
-rw-r--r--tactics/class_tactics.ml414
-rw-r--r--tactics/eauto.ml47
-rw-r--r--tactics/elimschemes.ml16
-rw-r--r--tactics/eqdecide.ml43
-rw-r--r--tactics/equality.ml2
-rw-r--r--tactics/extraargs.ml44
-rw-r--r--tactics/extratactics.ml49
-rw-r--r--tactics/hiddentac.ml1
-rw-r--r--tactics/hipattern.ml415
-rw-r--r--tactics/inv.ml1
-rw-r--r--tactics/nbtermdn.ml13
-rw-r--r--tactics/rewrite.ml413
-rw-r--r--tactics/tacinterp.ml22
-rw-r--r--tactics/tacticals.mli1
-rw-r--r--tactics/tactics.ml5
-rw-r--r--tactics/tauto.ml42
18 files changed, 1 insertions, 168 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index d88a6a6b0..748b608b4 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -22,7 +22,6 @@ open Pattern
open Patternops
open Matching
open Tacmach
-open Proof_type
open Pfedit
open Genredexpr
open Tacred
@@ -108,18 +107,6 @@ let insert v l =
type stored_data = int * pri_auto_tactic
(* First component is the index of insertion in the table, to keep most recent first semantics. *)
-let auto_tactic_ord code1 code2 =
- match code1, code2 with
- | Res_pf (c1, _), Res_pf (c2, _)
- | ERes_pf (c1, _), ERes_pf (c2, _)
- | Give_exact c1, Give_exact c2
- | Res_pf_THEN_trivial_fail (c1, _), Res_pf_THEN_trivial_fail (c2, _) -> constr_ord c1 c2
- | Unfold_nth (EvalVarRef i1), Unfold_nth (EvalVarRef i2) -> Pervasives.compare i1 i2
- | Unfold_nth (EvalConstRef c1), Unfold_nth (EvalConstRef c2) ->
- kn_ord (canonical_con c1) (canonical_con c2)
- | Extern t1, Extern t2 -> Pervasives.compare t1 t2
- | _ -> Pervasives.compare code1 code2
-
module Bounded_net = Btermdn.Make(struct
type t = stored_data
let compare = pri_order_int
@@ -436,8 +423,6 @@ module Hintdbmap = Gmap
type hint_db = Hint_db.t
-type frozen_hint_db_table = (string,hint_db) Hintdbmap.t
-
type hint_db_table = (string,hint_db) Hintdbmap.t ref
type hint_db_name = string
@@ -484,8 +469,6 @@ let try_head_pattern c =
try head_pattern_bound c
with BoundPattern -> error "Bound head variable."
-let name_of_constr c = try Some (global_of_constr c) with Not_found -> None
-
let make_exact_entry sigma pri ?(name=PathAny) (c,cty) =
let cty = strip_outer_cast cty in
match kind_of_term cty with
@@ -1393,22 +1376,6 @@ let possible_resolve dbg mod_delta db_list local_db cl =
let dbg_case dbg id =
tclLOG dbg (fun () -> str "case " ++ pr_id id) (simplest_case (mkVar id))
-let decomp_unary_term_then dbg (id,_,typc) kont1 kont2 gl =
- try
- let ccl = applist (head_constr typc) in
- match Hipattern.match_with_conjunction ccl with
- | Some (_,args) ->
- tclTHEN (dbg_case dbg id) (kont1 (List.length args)) gl
- | None ->
- kont2 gl
- with UserError _ -> kont2 gl
-
-let decomp_empty_term dbg (id,_,typc) gl =
- if Hipattern.is_empty_type typc then
- dbg_case dbg id gl
- else
- errorlabstrm "Auto.decomp_empty_term" (str "Not an empty type.")
-
let extend_local_db gl decl db =
Hint_db.add_list (make_resolve_hyp (pf_env gl) (project gl) decl) db
@@ -1422,8 +1389,6 @@ let intro_register dbg kont db =
(* n is the max depth of search *)
(* local_db contains the local Hypotheses *)
-exception Uplift of tactic list
-
let search d n mod_delta db_list local_db =
let rec search d n local_db =
if n=0 then (fun gl -> error "BOUND 2") else
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index dfa94102d..dd02475dd 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -242,12 +242,6 @@ type hypinfo = {
hyp_right : constr;
}
-let evd_convertible env evd x y =
- try
- ignore(Unification.w_unify ~flags:Unification.elim_flags env evd Reduction.CONV x y); true
- (* try ignore(Evarconv.the_conv_x env x y evd); true *)
- with _ -> false
-
let decompose_applied_relation metas env sigma c ctype left2right =
let find_rel ty =
let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 933bb6619..d411a28c4 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -12,29 +12,16 @@ open Pp
open Errors
open Util
open Names
-open Nameops
open Term
open Termops
-open Sign
open Reduction
open Proof_type
-open Declarations
open Tacticals
open Tacmach
-open Evar_refiner
open Tactics
-open Pattern
open Patternops
open Clenv
-open Auto
-open Glob_term
-open Hiddentac
open Typeclasses
-open Typeclasses_errors
-open Classes
-open Topconstr
-open Pfedit
-open Command
open Globnames
open Evd
open Locus
@@ -750,7 +737,6 @@ VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings
END
open Genarg
-open Extraargs
let pr_debug _prc _prlc _prt b =
if b then Pp.str "debug" else Pp.mt()
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 02d99d707..2bbb3ac5a 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -15,15 +15,10 @@ open Names
open Nameops
open Term
open Termops
-open Sign
-open Reduction
open Proof_type
-open Declarations
open Tacticals
open Tacmach
-open Evar_refiner
open Tactics
-open Pattern
open Patternops
open Clenv
open Auto
@@ -353,8 +348,6 @@ let e_search_auto debug (in_depth,p) lems db_list gl =
pr_info_nop d;
error "eauto: search failed"
-open Evd
-
let eauto_with_bases ?(debug=Off) np lems db_list =
tclTRY (e_search_auto debug np lems db_list)
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index fd21d84b0..62d13c0a6 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -58,10 +58,6 @@ let rect_dep_scheme_kind_from_type =
declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
(build_induction_scheme_in_type true InType)
-let rect_dep_scheme_kind_from_prop =
- declare_individual_scheme_object "_rect_dep"
- (build_induction_scheme_in_type true InType)
-
let ind_scheme_kind_from_type =
declare_individual_scheme_object "_ind_nodep"
(optimize_non_type_induction_scheme rect_scheme_kind_from_type false InProp)
@@ -74,14 +70,6 @@ let ind_dep_scheme_kind_from_type =
declare_individual_scheme_object "_ind" ~aux:"_ind_from_type"
(optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InProp)
-let ind_dep_scheme_kind_from_prop =
- declare_individual_scheme_object "_ind_dep"
- (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_prop true InProp)
-
-let rec_scheme_kind_from_type =
- declare_individual_scheme_object "_rec_nodep"
- (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet)
-
let rec_scheme_kind_from_prop =
declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop"
(optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet)
@@ -90,10 +78,6 @@ let rec_dep_scheme_kind_from_type =
declare_individual_scheme_object "_rec" ~aux:"_rec_from_type"
(optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet)
-let rec_dep_scheme_kind_from_prop =
- declare_individual_scheme_object "_rec_dep"
- (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_prop true InSet)
-
(* Case analysis *)
let build_case_analysis_scheme_in_type dep sort ind =
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index f26eb1024..5329029a8 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -23,12 +23,9 @@ open Declarations
open Tactics
open Tacticals
open Hiddentac
-open Equality
open Auto
-open Pattern
open Matching
open Hipattern
-open Proof_type
open Tacmach
open Coqlib
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 08b05746b..9827b6146 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -753,8 +753,6 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq =
let eq_elim = ind_scheme_of_eq lbeq in
(applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term)
-exception NotDiscriminable
-
let eq_baseid = id_of_string "e"
let apply_on_clause (f,t) clause =
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 33cbf1b2d..e0ba730cd 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -9,12 +9,10 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
open Pp
-open Pcoq
open Genarg
open Names
open Tacexpr
open Tacinterp
-open Termops
open Misctypes
open Locus
@@ -39,8 +37,6 @@ let pr_orient = pr_orient () () ()
let pr_int_list = Pp.pr_sequence Pp.int
let pr_int_list_full _prc _prlc _prt l = pr_int_list l
-open Glob_term
-
let pr_occurrences _prc _prlc _prt l =
match l with
| ArgArg x -> pr_int_list x
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 7f0e486ab..a3fa9956e 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -9,13 +9,11 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
open Pp
-open Pcoq
open Genarg
open Extraargs
open Mod_subst
open Names
open Tacexpr
-open Glob_term
open Glob_ops
open Tactics
open Errors
@@ -338,7 +336,6 @@ VERNAC COMMAND EXTEND DeriveInversionClear
END
open Term
-open Glob_term
VERNAC COMMAND EXTEND DeriveInversion
| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ]
@@ -389,7 +386,6 @@ TACTIC EXTEND evar
| [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ]
END
-open Tacexpr
open Tacticals
TACTIC EXTEND instantiate
@@ -403,8 +399,6 @@ END
(** Nijmegen "step" tactic for setoid rewriting *)
open Tactics
-open Tactics
-open Libnames
open Glob_term
open Summary
open Libobject
@@ -623,9 +617,6 @@ END
hget_evar
*)
-open Evar_refiner
-open Sign
-
let hget_evar n gl =
let sigma = project gl in
let evl = evar_list sigma (pf_concl gl) in
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 77379cb74..b68b6c545 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-
open Refiner
open Tacexpr
open Tactics
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 237c63a83..ec8bc5f7e 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -12,16 +12,9 @@ open Pp
open Errors
open Util
open Names
-open Nameops
open Term
-open Sign
open Termops
-open Reductionops
open Inductiveops
-open Evd
-open Environ
-open Clenv
-open Pattern
open Matching
open Coqlib
open Declarations
@@ -359,7 +352,6 @@ let coq_eq_pattern_gen eq = lazy PATTERN [ %eq ?X1 ?X2 ?X3 ]
let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref
let coq_identity_pattern = coq_eq_pattern_gen coq_identity_ref
let coq_jmeq_pattern = lazy PATTERN [ %coq_jmeq_ref ?X1 ?X2 ?X3 ?X4 ]
-let coq_eq_true_pattern = lazy PATTERN [ %coq_eq_true_ref ?X1 ]
let match_eq eqn eq_pat =
let pat = try Lazy.force eq_pat with _ -> raise PatternMatchingFailure in
@@ -392,12 +384,6 @@ let find_eq_data_decompose gl eqn =
let (lbeq,eq_args) = find_eq_data eqn in
(lbeq,extract_eq_args gl eq_args)
-let inversible_equalities =
- [coq_eq_pattern, build_coq_inversion_eq_data;
- coq_jmeq_pattern, build_coq_inversion_jmeq_data;
- coq_identity_pattern, build_coq_inversion_identity_data;
- coq_eq_true_pattern, build_coq_inversion_eq_true_data]
-
let find_this_eq_data_decompose gl eqn =
let (lbeq,eq_args) =
try (*first_match (match_eq eqn) inversible_equalities*)
@@ -411,7 +397,6 @@ let find_this_eq_data_decompose gl eqn =
(lbeq,eq_args)
open Tacmach
-open Tacticals
let match_eq_nf gls eqn eq_pat =
match pf_matches gls (Lazy.force eq_pat) eqn with
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 189c73a16..d598a97e6 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -198,7 +198,6 @@ let split_dep_and_nodep hyps gl =
if var_occurs_in_pf gl id then (d::l1,l2) else (l1,d::l2))
hyps ([],[])
-
(* Computation of dids is late; must have been done in rewrite_equations*)
(* Will keep generalizing and introducing back and forth... *)
(* Moreover, others hyps depending of dids should have been *)
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index 6459336b8..bafc85b12 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -104,19 +104,6 @@ let decomp =
| Const _ -> Dn.Everything
| _ -> Dn.Nothing
-let constr_val_discr_st (idpred,cpred) t =
- let c, l = decomp t in
- match kind_of_term c with
- | Const c -> if Cpred.mem c cpred then Dn.Everything else Dn.Label(Term_dn.GRLabel (ConstRef c),l)
- | Ind ind_sp -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l)
- | Construct cstr_sp -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l)
- | Var id when not (Idpred.mem id idpred) -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
- | Prod (n, d, c) -> Dn.Label(Term_dn.ProdLabel, [d; c])
- | Lambda (n, d, c) -> Dn.Label(Term_dn.LambdaLabel, [d; c] @ l)
- | Sort _ -> Dn.Label(Term_dn.SortLabel, [])
- | Evar _ -> Dn.Everything
- | _ -> Dn.Nothing
-
let lookup dn valu =
let hkey =
match (constr_val_discr valu) with
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index db2abea35..f2075d07d 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -16,26 +16,17 @@ open Nameops
open Namegen
open Term
open Termops
-open Sign
open Reduction
-open Proof_type
-open Declarations
open Tacticals
open Tacmach
-open Evar_refiner
open Tactics
-open Pattern
open Patternops
open Clenv
-open Auto
open Glob_term
-open Hiddentac
open Typeclasses
open Typeclasses_errors
open Classes
open Constrexpr
-open Pfedit
-open Command
open Libnames
open Globnames
open Evd
@@ -1345,9 +1336,7 @@ let cl_rewrite_clause l left2right occs clause gl =
cl_rewrite_clause_strat (rewrite_with (general_rewrite_unif_flags ()) l left2right occs) clause gl
open Pp
-open Pcoq
open Names
-open Tacexpr
open Tacinterp
open Termops
open Genarg
@@ -1380,8 +1369,6 @@ let interp_glob_constr_list env sigma =
let evd, c = Pretyping.understand_tcc sigma env c in
(evd, (c, NoBindings)), true)
-open Pcoq
-
(* Syntax for rewriting with strategies *)
type constr_expr_with_bindings = constr_expr with_bindings
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9bbb09589..0c7d6e0ca 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -7,7 +7,6 @@
(************************************************************************)
open Constrintern
-open Closure
open Libobject
open Pattern
open Patternops
@@ -147,14 +146,6 @@ let ((value_in : value -> Dyn.t),
(value_out : Dyn.t -> value)) = Dyn.create "value"
let valueIn t = TacDynamic (Loc.ghost,value_in t)
-let valueOut = function
- | TacDynamic (_,d) ->
- if (Dyn.tag d) = "value" then
- value_out d
- else
- anomalylabstrm "valueOut" (str "Dynamic tag should be value")
- | ast ->
- anomalylabstrm "valueOut" (str "Not a Dynamic ast: ")
(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
let atomic_mactab = ref Idmap.empty
@@ -1291,9 +1282,6 @@ let interp_constr = interp_constr_gen (OfType None)
let interp_type = interp_constr_gen IsType
(* Interprets an open constr *)
-let interp_open_constr_gen kind ist =
- interp_gen kind ist false true false false
-
let interp_open_constr ccl ist =
interp_gen (OfType ccl) ist false true false (ccl<>None)
@@ -3192,16 +3180,6 @@ let tacticIn t =
(str "Incorrect tactic expression. Received exception is:" ++
Errors.print e))
-let tacticOut = function
- | TacArg (_,TacDynamic (_,d)) ->
- if (Dyn.tag d) = "tactic" then
- tactic_out d
- else
- anomalylabstrm "tacticOut" (str "Dynamic tag should be tactic")
- | ast ->
- anomalylabstrm "tacticOut"
- (str "Not a Dynamic ast: " (* ++ print_ast ast*) )
-
(***************************************************************************)
(* Backwarding recursive needs of tactic glob/interp/eval functions *)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 39f60e196..61b80b584 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -52,6 +52,7 @@ val tclAT_LEAST_ONCE : tactic -> tactic
val tclFAIL : int -> std_ppcmds -> tactic
val tclFAIL_lazy : int -> std_ppcmds Lazy.t -> tactic
val tclDO : int -> tactic -> tactic
+val tclTIMEOUT : int -> tactic -> tactic
val tclWEAK_PROGRESS : tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclSHOWHYPS : tactic -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a29ab24ba..e55ba5d0e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1910,8 +1910,6 @@ let re_intro_dependent_hypotheses (lstatus,rstatus) (_,tophyp) =
(intros_move rstatus)
(intros_move newlstatus)
-let update destopt tophyp = if destopt = MoveLast then tophyp else destopt
-
let safe_dest_intros_patterns avoid thin dest pat tac gl =
try intros_patterns true avoid [] thin dest tac pat gl
with UserError ("move_hyp",_) ->
@@ -2650,9 +2648,6 @@ let rebuild_elimtype_from_scheme (scheme:elim_scheme): types =
paramconcl
-exception NoLastArg
-exception NoLastArgCcl
-
(* Builds an elim_scheme from its type and calling form (const+binding). We
first separate branches. We obtain branches, hyps before (params + preds),
hyps after (args <+ indarg if present>) and conclusion. Then we proceed as
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index fdfc2b783..afd0e7799 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -13,13 +13,11 @@ open Hipattern
open Names
open Globnames
open Pp
-open Proof_type
open Tacticals
open Tacinterp
open Tactics
open Errors
open Util
-open Genarg
let assoc_var s ist =
match List.assoc (Names.id_of_string s) ist.lfun with
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 10:29:55 +0000