From 855014ca4bbffd677ec1ce6ca938ab8f5134a9dd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 Oct 2016 09:07:51 +0200
Subject: [PATCH] =?UTF-8?q?ElimModal=20instance=20for=20=E2=96=A1.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 proofmode/class_instances.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index f03509b43..fb5b5de76 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -381,6 +381,9 @@ Proof.
   rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
 Qed.
 
+Global Instance elim_modal_always P Q : ElimModal (â–¡ P) P Q Q.
+Proof. intros. by rewrite /ElimModal always_elim wand_elim_r. Qed.
+
 Global Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q).
 Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
 
-- 
GitLab