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.

theories/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