From 95b3911c7dc50ab1cd9785524830253369417adc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 5 Mar 2017 20:49:25 +0100
Subject: [PATCH] Use strong framing for pure stuff.

---
 theories/proofmode/tactics.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index a9b8984e8..f48957c36 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -177,7 +177,8 @@ Local Ltac iFrameFinish :=
 Local Ltac iFramePure t :=
   let φ := type of t in
   eapply (tac_frame_pure _ _ _ _ t);
-    [apply _ || fail "iFrame: cannot frame" φ
+    [typeclasses eauto with typeclass_instances strong_frame
+     || fail "iFrame: cannot frame" φ
     |iFrameFinish].
 
 Local Ltac iFrameHyp strong H :=
-- 
GitLab