aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml4
-rw-r--r--tactics/class_tactics.ml18
-rw-r--r--tactics/equality.ml1
-rw-r--r--tactics/equality.mli6
-rw-r--r--tactics/rewrite.ml49
-rw-r--r--tactics/tacinterp.ml2
-rw-r--r--tactics/tacticMatching.ml3
-rw-r--r--tactics/tactics.ml5
8 files changed, 4 insertions, 84 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 795582f27..45f92a97f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -10,7 +10,6 @@ open Pp
open Errors
open Util
open Names
-open Nameops
open Namegen
open Term
open Vars
@@ -1420,9 +1419,6 @@ let possible_resolve dbg mod_delta db_list local_db cl =
(my_find_search mod_delta db_list local_db head cl)
with Not_found -> []
-let dbg_case dbg id =
- new_tclLOG dbg (fun () -> str "case " ++ pr_id id) (simplest_case (mkVar id))
-
let extend_local_db gl decl db =
Hint_db.add_list (make_resolve_hyp (pf_env gl) (project gl) decl) db
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c33e5fb7c..6d7c797af 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -28,13 +28,9 @@ open Proofview.Notations
(** Hint database named "typeclass_instances", now created directly in Auto *)
-let typeclasses_db = Auto.typeclasses_db
-
let typeclasses_debug = ref false
let typeclasses_depth = ref None
-exception Found of evar_map
-
(** We transform the evars that are concerned by this resolution
(according to predicate p) into goals.
Invariant: function p only manipulates and returns undefined evars *)
@@ -191,13 +187,10 @@ let e_possible_resolve db_list local_db gl =
(fst (head_constr_bound gl)) false gl
with Bound | Not_found -> []
-let rec catchable = function
+let catchable = function
| Refiner.FailError _ -> true
| e -> Logic.catchable_exception e
-let nb_empty_evars s =
- Evar.Map.cardinal (undefined_map s)
-
let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) (Evarutil.nf_evar evs (Goal.V82.concl evs ev))
let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l)
@@ -316,15 +309,6 @@ let normevars_tac : atac =
let info' = { info with auto_last_tac = lazy (str"normevars") } in
sk {it = [gl', info']; sigma = sigma';} fk }
-(* Ordering of states is lexicographic on the number of remaining goals. *)
-let compare (pri, _, _, res) (pri', _, _, res') =
- let nbgoals s =
- List.length (sig_it s) + nb_empty_evars (sig_sig s)
- in
- let pri = pri - pri' in
- if not (Int.equal pri 0) then pri
- else nbgoals res - nbgoals res'
-
let or_tac (x : 'a tac) (y : 'a tac) : 'a tac =
{ skft = fun sk fk gls -> x.skft sk (fun () -> y.skft sk fk gls) gls }
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 2854d1019..ff94937db 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -256,7 +256,6 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
*)
let (forward_general_rewrite_clause, general_rewrite_clause) = Hook.make ()
-let (forward_is_applied_rewrite_relation, is_applied_rewrite_relation) = Hook.make ()
(* Do we have a JMeq instance on twice the same domains ? *)
diff --git a/tactics/equality.mli b/tactics/equality.mli
index e8b142d89..681b366db 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -9,7 +9,6 @@
(*i*)
open Names
open Term
-open Context
open Evd
open Environ
open Tacmach
@@ -43,9 +42,8 @@ val rewriteRL : ?tac:(unit Proofview.tactic * conditions) -> constr -> unit Pro
(* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *)
val general_rewrite_clause :
- (Id.t option -> orientation ->
- occurrences -> constr with_bindings -> new_goals:constr list -> unit Proofview.tactic) Hook.t
-val is_applied_rewrite_relation : (env -> evar_map -> rel_context -> constr -> constr option) Hook.t
+ (Id.t option -> orientation -> occurrences -> constr with_bindings ->
+ new_goals:constr list -> unit Proofview.tactic) Hook.t
val general_rewrite_ebindings_clause : Id.t option ->
orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 79a1a41c8..ae73d7a41 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -18,7 +18,6 @@ open Reduction
open Tacticals
open Tacmach
open Tactics
-open Patternops
open Clenv
open Typeclasses
open Typeclasses_errors
@@ -127,10 +126,6 @@ let new_cstr_evar (evd,cstrs) env t =
let evd', t = Evarutil.new_evar evd env t in
(evd', Evar.Set.add (fst (destEvar t)) cstrs), t
-let new_goal_evar (evd,cstrs) env t =
- let evd', t = Evarutil.new_evar evd env t in
- (evd', cstrs), t
-
(** Building or looking up instances. *)
let proper_proof env evars carrier relation x =
@@ -225,9 +220,6 @@ let is_applied_rewrite_relation env sigma rels t =
with e when Errors.noncritical e -> None)
| _ -> None
-let _ =
- Hook.set Equality.is_applied_rewrite_relation is_applied_rewrite_relation
-
let rec decompose_app_rel env evd t =
match kind_of_term t with
| App (f, args) ->
@@ -541,10 +533,6 @@ type 'a pure_strategy = 'a -> Environ.env -> Id.t list -> constr -> types ->
type strategy = unit pure_strategy
-let get_rew_rel r = match r.rew_prf with
- | RewPrf (rel, prf) -> rel
- | RewCast c -> mkApp (Coqlib.build_coq_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 ->
@@ -717,12 +705,6 @@ let fold_match ?(force=false) env sigma c =
in
sk, (if exists then env else reset_env env), app, eff
-let fold_match_tac c gl =
- let _, _, c', eff = fold_match ~force:true (pf_env gl) (project gl) c in
- tclTHEN (Tactics.emit_side_effects eff)
- (change (Some (snd (pattern_of_constr (project gl) c))) c' onConcl) gl
-
-
let unfold_match env sigma sk app =
match kind_of_term app with
| App (f', args) when eq_constr f' (mkConst sk) ->
@@ -1044,23 +1026,6 @@ module Strategies =
state, Info { rew_car = ty; rew_from = t; rew_to = t';
rew_prf = RewCast ckind; rew_evars = evars }
- let fold c : 'a pure_strategy =
- fun state 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
- state, Info { rew_car = ty; rew_from = t; rew_to = c';
- rew_prf = RewCast DEFAULTcast;
- rew_evars = sigma, cstrevars evars }
- with e when Errors.noncritical e -> state, Fail
-
let fold_glob c : 'a pure_strategy =
fun state env avoid t ty cstr evars ->
(* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
@@ -1115,10 +1080,6 @@ let solve_constraints env evars =
let nf_zeta =
Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
-let map_rewprf f = function
- | RewPrf (rel, prf) -> RewPrf (f rel, f prf)
- | RewCast c -> RewCast c
-
exception RewriteFailure of std_ppcmds
type result = (evar_map * constr option * types) rewrite_result
@@ -1215,8 +1176,6 @@ let cl_rewrite_clause_tac ?abs strat clause gl =
let bind_gl_info f =
bind concl (fun c -> bind env (fun v -> bind defs (fun ev -> f c v ev)))
-let fail l s = Refiner.tclFAIL l s
-
let new_refine c : Goal.subgoals Goal.sensitive =
let refable = Goal.Refinable.make
(fun handle -> Goal.Refinable.constr_of_open_constr handle true c)
@@ -1329,14 +1288,6 @@ let cl_rewrite_clause_strat strat clause =
let cl_rewrite_clause l left2right occs clause gl =
cl_rewrite_clause_strat (rewrite_with left2right (general_rewrite_unif_flags ()) l 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)
-
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 l2r (general_rewrite_unif_flags ()) (c, NoBindings)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 60564dbdb..830fbd2d4 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -423,7 +423,7 @@ let rec intropattern_ids (loc,pat) = match pat with
| IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _
| IntroForthcoming _ -> []
-let rec extract_ids ids lfun =
+let extract_ids ids lfun =
let fold id v accu =
let v = Value.normalize v in
if has_type v (topwit wit_intro_pattern) then
diff --git a/tactics/tacticMatching.ml b/tactics/tacticMatching.ml
index 85108f8ed..b11841a65 100644
--- a/tactics/tacticMatching.ml
+++ b/tactics/tacticMatching.ml
@@ -215,9 +215,6 @@ module PatternMatching (E:StaticEnvironment) = struct
(** Declares a substitution. *)
let put_subst subst : unit m = put subst empty_context_subst empty_term_subst
- (** Declares a context substitution. *)
- let put_context context : unit m = put empty_subst context empty_term_subst
-
(** Declares a term substitution. *)
let put_terms terms : unit m = put empty_subst empty_context_subst terms
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index fda84e6f5..cb7a7b0d9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -67,14 +67,11 @@ let typ_of = Retyping.get_type_of
(* Option for 8.2 compatibility *)
open Goptions
let dependent_propositions_elimination = ref true
-let tactic_compat_context = ref false
let use_dependent_propositions_elimination () =
!dependent_propositions_elimination
&& Flags.version_strictly_greater Flags.V8_2
-let use_tactic_context_compat () = !tactic_compat_context
-
let _ =
declare_bool_option
{ optsync = true;
@@ -172,7 +169,6 @@ let internal_cut_rev_gen b d t gl =
with Evarutil.ClearDependencyError (id,err) ->
error_clear_dependency (pf_env gl) id err
-let internal_cut_rev = internal_cut_rev_gen false
let internal_cut_rev_replace = internal_cut_rev_gen true
(* Moving hypotheses *)
@@ -348,7 +344,6 @@ let change chg c cls gl =
cls gl
(* Pour usage interne (le niveau User est pris en compte par reduce) *)
-let try_red_in_concl = reduct_in_concl (try_red_product,REVERTcast)
let red_in_concl = reduct_in_concl (red_product,REVERTcast)
let red_in_hyp = reduct_in_hyp red_product
let red_option = reduct_option (red_product,REVERTcast)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 23:18:02 +0000