diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index a9b8984e8033489b7884cde454ebb5ff32b83f7e..f48957c36bb1b313c0a07d9f7e060a6d3b37ed5b 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 :=