From b917185865d0bfca6fde22fb6940aa4b8ca9f297 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 25 Feb 2016 12:07:54 +0100
Subject: [PATCH] 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 | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index 6f9cf631..6a8d64ad 100644
--- a/theories/tactics.v
+++ b/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 
-- 
GitLab