From b55c40d6f3f3b7843a8ea03d64a639f757205707 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.
---
 prelude/tactics.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/prelude/tactics.v b/prelude/tactics.v
index 9ca44595f..b335f5dfc 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 
-- 
GitLab