aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml15
-rw-r--r--tactics/coretactics.ml43
-rw-r--r--tactics/eauto.ml42
-rw-r--r--tactics/elimschemes.ml1
-rw-r--r--tactics/eqdecide.ml2
-rw-r--r--tactics/extraargs.ml43
-rw-r--r--tactics/hipattern.ml411
-rw-r--r--tactics/rewrite.ml135
-rw-r--r--tactics/tacintern.ml4
-rw-r--r--tactics/tacinterp.ml13
-rw-r--r--tactics/tacsubst.ml1
-rw-r--r--tactics/tacticals.mli2
-rw-r--r--tactics/tauto.ml41
-rw-r--r--tactics/term_dnet.ml4
14 files changed, 5 insertions, 192 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index aa70d55cc..4f5f53ef0 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -141,12 +141,6 @@ type search_entry = stored_data list * stored_data list * Bounded_net.t
let empty_se = ([],[],Bounded_net.create ())
-let eq_constr_or_reference x y =
- match x, y with
- | IsConstr (x,_), IsConstr (y,_) -> eq_constr x y
- | IsGlobRef x, IsGlobRef y -> eq_gr x y
- | _, _ -> false
-
let eq_pri_auto_tactic (_, x) (_, y) =
if Int.equal x.pri y.pri && Option.equal constr_pattern_eq x.pat y.pat then
match x.code,y.code with
@@ -189,11 +183,6 @@ let is_transparent_gr (ids, csts) = function
let dummy_goal = Goal.V82.dummy_goal
-let instantiate_constr_or_ref env sigma c =
- let c, ctx = Universes.fresh_global_or_constr_instance env c in
- let cty = Retyping.get_type_of env sigma c in
- (c, cty), ctx
-
let strip_params env c =
match kind_of_term c with
| App (f, args) ->
@@ -875,10 +864,6 @@ let (forward_intern_tac, extern_intern_tac) = Hook.make ()
type hnf = bool
-let pr_hint_term = function
- | IsConstr (c,_) -> pr_constr c
- | IsGlobRef gr -> pr_global gr
-
type hints_entry =
| HintsResolveEntry of (int option * polymorphic * hnf * hints_path_atom * hint_term) list
| HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index a95d71443..02dded782 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -9,11 +9,8 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
open Util
-open Names
open Locus
-open Tacexpr
open Misctypes
-open Tacinterp
DECLARE PLUGIN "coretactics"
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index bb7d2f0d2..fd5310e04 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -211,7 +211,7 @@ module SearchProblem = struct
let success s = List.is_empty (sig_it s.tacres)
- let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl)
+(* let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl) *)
let filter_tactics glls l =
(* let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 617475bb7..9b600409a 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -17,7 +17,6 @@ open Term
open Indrec
open Declarations
open Typeops
-open Termops
open Ind_tables
(* Induction/recursion schemes *)
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 7909b669b..c18fd31d0 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -82,8 +82,6 @@ let solveNoteqBranch side =
let make_eq () =
(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
-let make_eq_refl () =
-(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq_refl ())
let mkDecideEqGoal eqonleft op rectype c1 c2 =
let equality = mkApp(make_eq(), [|rectype; c1; c2|]) in
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index dc41cf8e3..a2a8675a8 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -72,9 +72,6 @@ let glob_occs ist l = l
let subst_occs evm l = l
-type occurrences_or_var = int list or_var
-type occurrences = int list
-
ARGUMENT EXTEND occurrences
PRINTED BY pr_int_list_full
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 130e66720..a8bcec288 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -387,12 +387,6 @@ let match_eq eqn eq_pat =
let no_check () = true
let check_jmeq_loaded () = Library.library_is_loaded Coqlib.jmeq_module
-let build_coq_jmeq_data_in env =
- build_coq_jmeq_data (), Univ.ContextSet.empty
-
-let build_coq_identity_data_in env =
- build_coq_identity_data (), Univ.ContextSet.empty
-
let equalities =
[coq_eq_pattern, no_check, build_coq_eq_data;
coq_jmeq_pattern, check_jmeq_loaded, build_coq_jmeq_data;
@@ -442,11 +436,6 @@ let dest_nf_eq gls eqn =
(*** Sigma-types *)
-(* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *)
-let coq_ex_pattern_gen ex = lazy PATTERN [ %ex ?X1 ?X2 ?X3 ?X4 ]
-let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref
-let coq_exist_pattern = coq_ex_pattern_gen coq_exist_ref
-
let match_sigma ex =
match kind_of_term ex with
| App (f, [| a; p; car; cdr |]) when is_global (Lazy.force coq_exist_ref) f ->
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 7309e2275..b4b8d468c 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -36,12 +36,7 @@ open Goal
open Environ
open Tacinterp
open Termops
-open Genarg
-open Extraargs
-open Pcoq.Constr
-open Entries
open Libnames
-open Evarutil
(** Typeclass-based generalized rewriting. *)
@@ -76,7 +71,6 @@ let find_global dir s =
(** Global constants. *)
-let gen_reference dir s = Coqlib.gen_reference "rewrite" dir s
let coq_eq_ref = find_reference ["Init"; "Logic"] "eq"
let coq_eq = find_global ["Init"; "Logic"] "eq"
let coq_f_equal = find_global ["Init"; "Logic"] "f_equal"
@@ -118,13 +112,6 @@ let new_cstr_evar (evd,cstrs) env t =
let e_new_cstr_evar evars env t =
let evd', t = new_cstr_evar !evars env t in evars := evd'; t
-let new_goal_evar (evd,cstrs) env t =
- let evd', t = Evarutil.new_evar evd env t in
- (evd', cstrs), t
-
-let e_new_goal_evar evars env t =
- let evd', t = new_goal_evar !evars env t in evars := evd'; t
-
(** Building or looking up instances. *)
let extends_undefined evars evars' =
@@ -161,7 +148,6 @@ module GlobalBindings (M : sig
val relation : string list * string
val app_poly : env -> evars -> (evars -> evars * constr) -> constr array -> evars * constr
val arrow : evars -> evars * constr
- val coq_inverse : evars -> evars * constr
end) = struct
open M
let relation : evars -> evars * constr = find_global (fst relation) (snd relation)
@@ -608,14 +594,6 @@ let solve_remaining_by by env prf =
indep env.evd
in { env with evd = evd' }, prf
-let extend_evd sigma ext sigma' =
- Evar.Set.fold (fun i acc ->
- Evd.add acc i (Evarutil.nf_evar_info sigma' (Evd.find sigma' i)))
- ext sigma
-
-let shrink_evd sigma ext =
- Evar.Set.fold (fun i acc -> Evd.remove acc i) ext sigma
-
let no_constraints cstrs =
fun ev _ -> not (Evar.Set.mem ev cstrs)
@@ -707,10 +685,6 @@ let make_eq () =
let make_eq_refl () =
(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq_refl ())
-let get_rew_rel r = match r.rew_prf with
- | RewPrf (rel, prf) -> rel
- | RewCast c -> mkApp (make_eq (),[| r.rew_car; r.rew_from; r.rew_to |])
-
let get_rew_prf r = match r.rew_prf with
| RewPrf (rel, prf) -> rel, prf
| RewCast c ->
@@ -1289,25 +1263,6 @@ module Strategies =
Some (Some { rew_car = ty; rew_from = t; rew_to = t';
rew_prf = RewCast ckind; rew_evars = evars })
- let fold c : strategy =
- fun env avoid t ty cstr evars ->
-(* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
- let sigma, c = Constrintern.interp_open_constr (goalevars evars) env c in
- let unfolded =
- try Tacred.try_red_product env sigma c
- with e when Errors.noncritical e ->
- error "fold: the term is not unfoldable !"
- in
- try
- let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ())
- unfolded t in
- let c' = Evarutil.nf_evar sigma c in
- Some (Some { rew_car = ty; rew_from = t; rew_to = c';
- rew_prf = RewCast DEFAULTcast;
- rew_evars = (sigma, snd evars) })
- with e when Errors.noncritical e -> None
-
-
let fold_glob c : strategy =
fun env avoid t ty cstr evars ->
(* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
@@ -1426,9 +1381,6 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
| Some None -> Some None
| None -> None
-let rewrite_refine (evd,c) =
- Tacmach.refine c
-
let cl_rewrite_clause_tac ?abs strat meta clause gl =
let evartac evd = Refiner.tclEVARS (Evd.clear_metas evd) in
let treat res =
@@ -1582,30 +1534,11 @@ let cl_rewrite_clause_strat strat clause =
let cl_rewrite_clause l left2right occs clause gl =
cl_rewrite_clause_strat (rewrite_with (general_rewrite_unif_flags ()) l left2right occs) clause gl
-let occurrences_of = function
- | n::_ as nl when n < 0 -> (false,List.map abs nl)
- | nl ->
- if List.exists (fun n -> n < 0) nl then
- error "Illegal negative occurrence number.";
- (true,nl)
-
-open Extraargs
-
-let apply_constr_expr c l2r occs = fun env avoid t ty cstr evars ->
- let evd, c = Constrintern.interp_open_constr (goalevars evars) env c in
- apply_lemma (general_rewrite_unif_flags ()) (Evd.empty, (c, NoBindings))
- l2r None occs env avoid t ty cstr (evd, cstrevars evars)
-
let apply_glob_constr c l2r occs = fun env avoid t ty cstr evars ->
let evd, c = (Pretyping.understand_tcc (goalevars evars) env c) in
apply_lemma (general_rewrite_unif_flags ()) (Evd.empty, (c, NoBindings))
l2r None occs env avoid t ty cstr (evd, cstrevars evars)
-let interp_constr_list env sigma =
- List.map (fun c ->
- let evd, c = Constrintern.interp_open_constr sigma env c in
- (evd, (c, NoBindings)), true, None)
-
let interp_glob_constr_list env sigma =
List.map (fun c ->
let evd, c = Pretyping.understand_tcc sigma env c in
@@ -2112,74 +2045,6 @@ let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry
let _ = Hook.set Tactics.setoid_symmetry_in setoid_symmetry_in
let _ = Hook.set Tactics.setoid_transitivity setoid_transitivity
-let implify id gl =
- let (_, b, ctype) = pf_get_hyp gl id in
- let binders,concl = decompose_prod_assum ctype in
- let evm, ctype' =
- match binders with
- | (_, None, ty as hd) :: tl when noccurn 1 concl ->
- let env = Environ.push_rel_context tl (pf_env gl) in
- let sigma = project gl in
- let tyhd = Retyping.get_type_of env sigma ty
- and tyconcl = Retyping.get_type_of (Environ.push_rel hd env) sigma concl in
- let ((sigma,_), app), unfold =
- PropGlobal.arrow_morphism env (sigma, Evar.Set.empty) tyhd
- (subst1 mkProp tyconcl) ty (subst1 mkProp concl)
- in
- sigma, it_mkProd_or_LetIn app tl
- | _ -> project gl, ctype
- in tclTHEN (Refiner.tclEVARS evm) (Tacmach.convert_hyp (id, b, ctype')) gl
-
-let rec fold_matches env sigma c =
- map_constr_with_full_binders Environ.push_rel
- (fun env c ->
- match kind_of_term c with
- | Case _ ->
- let cst, env, c', _eff = fold_match ~force:true env sigma c in
- fold_matches env sigma c'
- | _ -> fold_matches env sigma c)
- env c
-
-let fold_match_tac c gl =
- let _, _, c', eff = fold_match ~force:true (pf_env gl) (project gl) c in
- let gl = { gl with sigma = Evd.emit_side_effects eff gl.sigma } in
- change (Some (snd (Patternops.pattern_of_constr (project gl) c))) c' onConcl gl
-
-let fold_matches_tac c gl =
- let c' = fold_matches (pf_env gl) (project gl) c in
- (* let gl = { gl with sigma = Evd.emit_side_effects eff gl.sigma } in *)
- change (Some (snd (Patternops.pattern_of_constr (project gl) c))) c' onConcl gl
-
-let myapply id l gl =
- let gr = id in
- let _, impls = List.hd (Impargs.implicits_of_global gr) in
- let env = pf_env gl in
- let evars = ref (project gl) in
- let evd, ty = fresh_global env !evars gr in
- let _ = evars := evd in
- let app =
- let rec aux ty impls args args' =
- match impls, kind_of_term ty with
- | Some (_, _, (_, _)) :: impls, Prod (n, t, t') ->
- let arg = Evarutil.e_new_evar evars env t in
- aux (subst1 arg t') impls args (arg :: args')
- | None :: impls, Prod (n, t, t') ->
- (match args with
- | [] ->
- if dependent (mkRel 1) t' then
- let arg = Evarutil.e_new_evar evars env t in
- aux (subst1 arg t') impls args (arg :: args')
- else
- let arg = Evarutil.mk_new_meta () in
- evars := meta_declare (destMeta arg) t !evars;
- aux (subst1 arg t') impls args (arg :: args')
- | arg :: args ->
- aux (subst1 arg t') impls args (arg :: args'))
- | _, _ -> mkApp (Universes.constr_of_global gr, Array.of_list (List.rev args'))
- in aux ty impls l []
- in
- tclTHEN (Refiner.tclEVARS !evars) (apply app) gl
-
let get_lemma_proof f env evm x y =
let (evm, _), c = f env (evm,Evar.Set.empty) x y in
evm, c
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 35952c9dd..f68f75359 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -43,10 +43,6 @@ let error_syntactic_metavariables_not_allowed loc =
let error_tactic_expected loc =
user_err_loc (loc,"",str "Tactic expected.")
-let skip_metaid = function
- | AI x -> x
- | MetaId (loc,_) -> error_syntactic_metavariables_not_allowed loc
-
(** Generic arguments *)
type glob_sign = Genintern.glob_sign = {
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b7018fe45..1d76f4afd 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -294,9 +294,6 @@ let interp_ident = interp_ident_gen false
let interp_fresh_ident = interp_ident_gen true
let pf_interp_ident id gl = interp_ident_gen false id (pf_env gl)
-let interp_global ist gl gr =
- Evd.fresh_global (pf_env gl) (project gl) gr
-
(* Interprets an optional identifier which must be fresh *)
let interp_fresh_name ist env = function
| Anonymous -> Anonymous
@@ -578,14 +575,6 @@ let interp_auto_lemmas ist env sigma lems =
let pf_interp_type ist gl =
interp_type ist (pf_env gl) (project gl)
-let new_interp_type ist c k =
- let open Proofview.Goal in
- let open Proofview.Notations in
- Proofview.Goal.raw_enter begin fun gl ->
- let (sigma, c) = interp_type ist (env gl) (sigma gl) c in
- Proofview.V82.tclEVARS sigma <*> k c
- end
-
(* Interprets a reduction expression *)
let interp_unfold ist env (occs,qid) =
(interp_occurrences ist occs,interp_evaluable ist env qid)
@@ -953,8 +942,6 @@ struct
Proofview.tclDISPATCHL (List.map f l) >>= fun l ->
Proofview.tclUNIT (Depends (List.concat l))
- let goal = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)
-
let enter f =
bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l))
(fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl))
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index aa090b715..4dd4b0aa8 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -15,7 +15,6 @@ open Misctypes
open Globnames
open Term
open Genredexpr
-open Inductiveops
open Patternops
open Pretyping
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index cc1528797..48fd44b4a 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -224,6 +224,8 @@ module New : sig
val onLastHyp : (constr -> unit tactic) -> unit tactic
val onLastDecl : (named_declaration -> unit tactic) -> unit tactic
+ val onHyps : ([ `NF ] Proofview.Goal.t -> named_context) ->
+ (named_context -> unit tactic) -> unit tactic
val afterHyp : Id.t -> (named_context -> unit tactic) -> unit tactic
val tryAllHyps : (identifier -> unit tactic) -> unit tactic
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 2d9b4da96..bdacf85a8 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -11,7 +11,6 @@
open Term
open Hipattern
open Names
-open Globnames
open Pp
open Genarg
open Stdarg
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index e05f4bcfe..f8d7a197b 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -337,11 +337,11 @@ struct
| _ -> assert false
(* debug *)
- let rec pr_term_pattern p =
+(* let rec pr_term_pattern p =
(fun pr_t -> function
| Term t -> pr_t t
| Meta m -> str"["++Pp.int (Obj.magic m)++str"]"
- ) (pr_dconstr pr_term_pattern) p
+ ) (pr_dconstr pr_term_pattern) p*)
let search_pat cpat dpat dn =
let whole_c = cpat in
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 15:05:16 +0000