From 37f022e4ea007a45cfdfcaac9e7114b53c1112a1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 25 Nov 2016 13:49:04 +0100
Subject: [PATCH] Make iLeft and iRight work with later.

---
 base_logic/lib/boxes.v      | 1 -
 proofmode/class_instances.v | 3 +++
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/base_logic/lib/boxes.v b/base_logic/lib/boxes.v
index 4a72231c0..22c010f75 100644
--- a/base_logic/lib/boxes.v
+++ b/base_logic/lib/boxes.v
@@ -276,7 +276,6 @@ Proof.
     eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
     iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
 Qed.
-
 End box.
 
 Typeclasses Opaque slice box.
diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index 5edcb5d02..2d0ebc397 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -330,6 +330,9 @@ 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_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.
 
 (* IntoOr *)
 Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
-- 
GitLab