Missing timeless instances.

efd5e13e · Robbert Krebbers · Jacques-Henri Jourdan · f0e57c42 · efd5e13e
Commit efd5e13e authored Sep 07, 2017 by Robbert Krebbers Committed by Jacques-Henri Jourdan Oct 31, 2017
Hide whitespace changes
Inline Side-by-side

Showing with 6 additions and 0 deletions

theories/bi/derived.v theories/bi/derived.v +6 -0

No files found.
--- 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.