From 5380a1d7eb145287d0b1d6538dad5e8ec01d8663 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 8 Mar 2021 13:05:41 +0100
Subject: [PATCH] fix build on Coq 8.11

---
 iris/base_logic/lib/gen_heap.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 4f59ad506..53928daf7 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -291,8 +291,8 @@ Lemma gen_heap_init_names `{Countable L, !gen_heapPreG L V Σ} σ :
     let hG := GenHeapG L V Σ γh γm in
     gen_heap_interp σ ∗ ([∗ map] l ↦ v ∈ σ, l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ, meta_token l ⊤).
 Proof.
-  iMod (ghost_map_alloc_empty (V:=V)) as (γh) "Hh".
-  iMod (ghost_map_alloc_empty (V:=gname)) as (γm) "Hm".
+  iMod (ghost_map_alloc_empty (K:=L) (V:=V)) as (γh) "Hh".
+  iMod (ghost_map_alloc_empty (K:=L) (V:=gname)) as (γm) "Hm".
   iExists γh, γm.
   iAssert (gen_heap_interp (hG:=GenHeapG _ _ _ γh γm) ∅) with "[Hh Hm]" as "Hinterp".
   { iExists ∅; simpl. iFrame "Hh Hm". by rewrite dom_empty_L. }
-- 
GitLab