From 26ae0c67ca3e0dacedb957709c9526e66741e55d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 25 Nov 2016 13:52:08 +0100
Subject: [PATCH] Make iLeft and iRight work with always.

---
 proofmode/class_instances.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index 2d0ebc397..35a8f6d4e 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -330,9 +330,12 @@ Proof. done. Qed.
 Global Instance from_or_bupd P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (|==> P) (|==> Q1) (|==> Q2).
 Proof. rewrite /FromOr=><-. apply or_elim; apply bupd_mono; auto with I. Qed.
+Global Instance from_or_always P Q1 Q2 :
+  FromOr P Q1 Q2 → FromOr (□ P) (□ Q1) (□ Q2).
+Proof. rewrite /FromOr=> <-. by rewrite always_or. Qed.
 Global Instance from_or_later P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (▷ P) (▷ Q1) (▷ Q2).
-Proof. rewrite /FromOr=><-. apply or_elim; apply later_mono; auto with I. Qed.
+Proof. rewrite /FromOr=><-. by rewrite later_or. Qed.
 
 (* IntoOr *)
 Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
-- 
GitLab