From ed7717fe1266fa15fbbf1f3741ace2e9e30f6281 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 beb49c8a0..1203e90a4 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -777,6 +777,12 @@ 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.
 
+Global Instance elim_modal_bupd_plain_goal P Q : PlainP 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 : PlainP 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