From 66f8aa36a2045016599288fb78ac297345c665cd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 5 Jan 2017 11:11:51 +0100
Subject: [PATCH] =?UTF-8?q?eauto=20hint=20for=20introducing=20=E2=97=87.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 02c4e2281..e535ccaaa 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.
-- 
GitLab