From 73997f2784c41f2388221ea1cc0b7b7866a9e140 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 13 Apr 2016 13:39:47 +0200
Subject: [PATCH] Make it compile with ssreflect master

---
 tests/heap_lang.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 4da765fb3..f10a57d99 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -70,6 +70,6 @@ Section ClosedProofs.
   Proof.
     iProof. iIntros "! Hσ".
     iPvs (heap_alloc nroot) "Hσ" as {h} "[? _]"; first by rewrite nclose_nroot.
-    by iApply heap_e_spec; first by rewrite nclose_nroot.
+    iApply heap_e_spec; last done ; by rewrite nclose_nroot.
   Qed.
 End ClosedProofs.
-- 
GitLab