From d7934c502d9ba461a0455352a76826b928a5bc37 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 22 Oct 2017 19:18:02 +0200
Subject: [PATCH] Proof mode instances for eliminating plain basic updates.

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

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index f6b67352e..72f872b81 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -815,6 +815,12 @@ Proof. intros. by rewrite /ElimModal persistently_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.
 
+Global Instance elim_modal_bupd_plain_goal P Q : Plain Q → ElimModal (|==> P) P Q Q.
+Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
+
+Global Instance elim_modal_bupd_plain P Q : Plain P → ElimModal (|==> P) P Q Q.
+Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
+
 Global Instance elim_modal_except_0 P Q : IsExcept0 Q → ElimModal (◇ P) P Q Q.
 Proof.
   intros. rewrite /ElimModal (except_0_intro (_ -∗ _)).
-- 
GitLab