diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index bee9749c2e9a1047a44e1f71509bca977b048b17..268d813e47b914700ef9604e28754773518a93bb 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1984,6 +1984,7 @@ Hint Extern 1 (envs_entails _ (â—‡ _)) => iModIntro.
 Hint Extern 1 (envs_entails _ (_ ∨ _)) => iLeft.
 Hint Extern 1 (envs_entails _ (_ ∨ _)) => iRight.
 Hint Extern 1 (envs_entails _ (|==> _)) => iModIntro.
+Hint Extern 1 (envs_entails _ (<absorb> _)) => iModIntro.
 Hint Extern 2 (envs_entails _ (|={_}=> _)) => iModIntro.
 
 Hint Extern 2 (envs_entails _ (_ ∗ _)) => progress iFrame : iFrame.