Commit 37f022e4 authored by Robbert Krebbers's avatar Robbert Krebbers

Make iLeft and iRight work with later.

parent f2bf449c
......@@ -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.
......@@ -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.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment