From af752fbedfc1803d73181a21ab364728cd8eb91a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 10 Nov 2020 19:41:31 +0100
Subject: [PATCH] fix build on older Coq

---
 theories/base_logic/lib/gen_heap.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 758234e4c..d368da7b6 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -300,7 +300,7 @@ Proof.
   { exact: gmap_view_auth_valid. }
   pose (gen_heap := GenHeapG L V Σ _ _ _ _ _ γh γm).
   iExists gen_heap.
-  iAssert (gen_heap_interp ∅) with "[Hh Hm]" as "Hinterp".
+  iAssert (gen_heap_interp (hG:=gen_heap) ∅) with "[Hh Hm]" as "Hinterp".
   { iExists ∅; simpl. iFrame "Hh Hm". by rewrite dom_empty_L. }
   iMod (gen_heap_alloc_big with "Hinterp") as "(Hinterp & $ & $)".
   { apply map_disjoint_empty_r. }
-- 
GitLab