diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 02c4e2281d9af91361b00cf0d6ae4221aa8f777a..e535ccaaa512df2ef2fd4c0be3f8b79efe8119ba 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1280,6 +1280,7 @@ Hint Extern 1 (of_envs _ ⊢ _) =>
   | |- _ ⊢ □ _ => iClear "*"; iAlways
   | |- _ ⊢ ∃ _, _ => iExists _
   | |- _ ⊢ |==> _ => iModIntro
+  | |- _ ⊢ ◇ _ => iModIntro
   end.
 Hint Extern 1 (of_envs _ ⊢ _) =>
   match goal with |- _ ⊢ (_ ∨ _)%I => iLeft end.