From 57b5f2a30ece6990e31df856be353fef0ffda2f4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 14 Dec 2016 14:55:16 +0100
Subject: [PATCH] fix build with coq 8.5
---
theories/lang/heap.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 284afe79..519b83c2 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -226,10 +226,10 @@ Section heap.
rewrite -!min_assoc min_idempotent min_comm -min_assoc min_idempotent min_comm. done. }
iDestruct "Hown" as "[H Hown]". iDestruct "H" as %Hl. iExists (take ll vl1). iFrame.
destruct (min_spec (length vl1) (length vl2)) as [[Hne Heq]|[Hne Heq]].
- + iClear "HP2". rewrite firstn_all2; last first.
+ + iClear "HP2". rewrite take_ge; last first.
{ rewrite -Heq /ll. done. }
rewrite drop_ge; first by rewrite app_nil_r. by rewrite -Heq.
- + iClear "HP1". rewrite Hl firstn_all2; last first.
+ + iClear "HP1". rewrite Hl take_ge; last first.
{ rewrite -Heq /ll. done. }
rewrite drop_ge; first by rewrite app_nil_r. by rewrite -Heq.
Qed.
--
GitLab