Commit b55c40d6 authored by Ralf Jung's avatar Ralf Jung

let find_pat treat "Typeclass Opaque" definitions opaquely

In principle, we could now un-seal heap_mapsto, saved_prop_own etc., and mark them as "Typeclass Opaque", and ecancel would still work just as fast as it does now.
Thanks to Matthieu for pointing me to this unify feature.
parent 9aed61c5
......@@ -389,7 +389,8 @@ It will search for the first subterm of the goal matching [pat], and then call [
with that subterm. *)
Ltac find_pat pat tac :=
match goal with |- context [?x] =>
unify pat x; tryif tac x then idtac else fail 2
unify pat x with typeclass_instances;
tryif tac x then idtac else fail 2
end.
(** Coq's [firstorder] tactic fails or loops on rather small goals already. In
......
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