diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 364a2b76257149fc30d10c4745eb8df2648064aa..dbd4d37864990abd61508d649ddb61912d7d42f4 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1322,3 +1322,5 @@ Hint Extern 1 (of_envs _ ⊢ |==> _) => iModIntro.
 Hint Extern 1 (of_envs _ ⊢ ◇ _) => iModIntro.
 Hint Extern 1 (of_envs _ ⊢ _ ∨ _) => iLeft.
 Hint Extern 1 (of_envs _ ⊢ _ ∨ _) => iRight.
+
+Hint Extern 2 (coq_tactics.of_envs _ ⊢ _ ∗ _) => progress iFrame : iFrame.