Add the `TimelessP (j ⤇ e)` instance.

6b01a6cf · Dan Frumin · a0de8ddf · 6b01a6cf
Commit 6b01a6cf authored Sep 26, 2017 by Dan Frumin
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 0 deletions

theories/logrel/threadpool.v theories/logrel/threadpool.v +2 -0

No files found.
--- a/theories/logrel/threadpool.v
+++ b/theories/logrel/threadpool.v
@@ -46,6 +46,8 @@ Section definitionsS.

  Global Instance heapS_mapsto_timeless l q v : TimelessP (heapS_mapsto l q v).
  Proof. rewrite heapS_mapsto_eq. apply _. Qed.
+  Global Instance tpool_mapsto_timeless j e: TimelessP (tpool_mapsto j e).
+  Proof. rewrite tpool_mapsto_eq. apply _. Qed.
  Global Instance spec_ctx_persistent ρ : PersistentP (spec_ctx ρ).
  Proof. apply _. Qed.
 End definitionsS.