From 985f97130ddb62e225e5026d213cc2ff55e14f1d Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 9 Mar 2018 13:18:58 +0100
Subject: [PATCH] Add hint for introducing absorbingly.

---
 theories/proofmode/tactics.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index bee9749c2..268d813e4 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.
-- 
GitLab