Commit eddfc645 authored by Robbert Krebbers's avatar Robbert Krebbers

Use ndot_ne_disjoint more eager so it expands definitions.

parent 0a1cf07d
......@@ -412,10 +412,11 @@ Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
It will search for the first subterm of the goal matching [pat], and then call [tac]
with that subterm. *)
Ltac find_pat pat tac :=
match goal with |- context [?x] =>
match goal with
|- context [?x] =>
unify pat x with typeclass_instances;
tryif tac x then idtac else fail 2
end.
end.
(** Coq's [firstorder] tactic fails or loops on rather small goals already. In
particular, on those generated by the tactic [unfold_elem_ofs] which is used
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment