From efd5e13ec22b9cf60c1ecd1c2b12647c2a29726b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 7 Sep 2017 13:38:13 +0200
Subject: [PATCH] Missing timeless instances.

---
 theories/bi/derived.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index ac2f1d3eb..653323888 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -1713,6 +1713,12 @@ Proof.
   by rewrite (timeless P) /bi_except_0 persistently_or {1}persistently_elim.
 Qed.
 
+Global Instance bare_timeless P :
+  Timeless (emp%I : PROP) → Timeless P → Timeless (■ P).
+Proof. rewrite /bi_bare; apply _. Qed.
+Global Instance sink_timeless P : Timeless P → Timeless (▲ P).
+Proof. rewrite /bi_sink; apply _. Qed.
+
 Global Instance eq_timeless {A : ofeT} (a b : A) :
   Discrete a → Timeless (a ≡ b : PROP)%I.
 Proof. intros. rewrite /Discrete !discrete_eq. apply (timeless _). Qed.
-- 
GitLab