diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 3 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 8 | ||||
| -rw-r--r-- | tactics/hints.ml | 21 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 3 |
4 files changed, 0 insertions, 35 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index e6263f92c..d6552920f 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -67,9 +67,6 @@ let auto_unif_flags_of st1 st2 useeager = let auto_unif_flags = auto_unif_flags_of full_transparent_state empty_transparent_state false -let auto_flags_of_state st = - auto_unif_flags_of full_transparent_state st false - (* Try unification with the precompiled clause, then use registered Apply *) let connect_hint_clenv poly (c, _, ctx) clenv gl = diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 4f0ffa024..8cd7b1ad6 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -569,14 +569,6 @@ let rec fix_limit limit (t : 'a tac) : 'a tac = if Int.equal limit 0 then fail_tac ReachedLimit else then_tac t { skft = fun sk fk -> (fix_limit (pred limit) t).skft sk fk } -let fix_iterative' t = - let rec aux depth = - { skft = fun sk fk gls -> - (fix_limit depth t).skft sk - (function NotApplicable as e -> fk e - | ReachedLimit -> (aux (succ depth)).skft sk fk gls) gls } - in aux 1 - let fix_iterative t = let rec aux depth = or_else_tac (fix_limit depth t) diff --git a/tactics/hints.ml b/tactics/hints.ml index 6d623f1c3..8d8b5fcc6 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -154,27 +154,6 @@ let fresh_key = in KerName.make mp dir (Label.of_id lbl) -let eq_hints_path_atom p1 p2 = match p1, p2 with -| PathHints gr1, PathHints gr2 -> List.equal eq_gr gr1 gr2 -| PathAny, PathAny -> true -| (PathHints _ | PathAny), _ -> false - -let eq_auto_tactic t1 t2 = match t1, t2 with -| Res_pf (c1, _), Res_pf (c2, _) -> Constr.equal c1 c2 -| ERes_pf (c1, _), ERes_pf (c2, _) -> Constr.equal c1 c2 -| Give_exact (c1, _), Give_exact (c2, _) -> Constr.equal c1 c2 -| Res_pf_THEN_trivial_fail (c1, _), Res_pf_THEN_trivial_fail (c2, _) -> Constr.equal c1 c2 -| Unfold_nth gr1, Unfold_nth gr2 -> eq_egr gr1 gr2 -| Extern tac1, Extern tac2 -> tac1 == tac2 (** May cause redundancy in addkv *) -| (Res_pf _ | ERes_pf _ | Give_exact _ | Res_pf_THEN_trivial_fail _ - | Unfold_nth _ | Extern _), _ -> false - -let eq_hint_metadata t1 t2 = - Int.equal t1.pri t2.pri && - Option.equal constr_pattern_eq t1.pat t2.pat && - eq_hints_path_atom t1.name t2.name && - eq_auto_tactic t1.code t2.code - let pri_order_int (id1, {pri=pri1}) (id2, {pri=pri2}) = let d = pri1 - pri2 in if Int.equal d 0 then id2 - id1 diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a87181588..5450a00f4 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1115,9 +1115,6 @@ let rec read_match_rule lfun ist env sigma = function (* misc *) -let mk_hyp_value ist env sigma c = - (mkVar (interp_hyp ist env sigma c)) - let interp_focussed wit f v = Ftactic.nf_enter begin fun gl -> let v = Genarg.out_gen (glbwit wit) v in |