From 3c054eb5d78965f92a76f229285009081422700f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Mar 2016 02:36:57 +0100
Subject: [PATCH] Mapsto is timeless.

---
 heap_lang/heap.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 19a7b2b69..d5576fe50 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -116,6 +116,9 @@ Section heap.
   Context `{heapG Σ}.
 
   (** General properties of mapsto *)
+  Global Instance heap_mapsto_timeless l q v : TimelessP (l ↦{q} v).
+  Proof. rewrite /heap_mapsto. apply _. Qed.
+
   Lemma heap_mapsto_op_eq l q1 q2 v :
     (l ↦{q1} v ★ l ↦{q2} v) ⊣⊢ (l ↦{q1+q2} v).
   Proof. by rewrite -auth_own_op map_op_singleton Frac_op dec_agree_idemp. Qed.
-- 
GitLab