From 784e2431db91f624dcf1e3f91d0e3182c7449a88 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 13 Aug 2019 13:31:18 +0200
Subject: [PATCH] add timeless instance

---
 theories/heap_lang/array.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/heap_lang/array.v b/theories/heap_lang/array.v
index 415f1cb76..15331b9e8 100644
--- a/theories/heap_lang/array.v
+++ b/theories/heap_lang/array.v
@@ -28,6 +28,8 @@ Implicit Types vs : list val.
 Implicit Types l : loc.
 Implicit Types sz off : nat.
 
+Global Instance array_timeless l vs : Timeless (array l vs) := _.
+
 Lemma array_nil l : l ↦∗ [] ⊣⊢ emp.
 Proof. by rewrite /array. Qed.
 
-- 
GitLab