diff --git a/prelude/tactics.v b/prelude/tactics.v index 9ca44595f581ce226a51d223260f5d1312af69ee..b335f5dfcc5d225bbae2bb9cd6d65950b95d6cc0 100644 --- a/prelude/tactics.v +++ b/prelude/tactics.v @@ -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