From 63ed680f6b4d5ff9fc386af9d657d36f9551bbba Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 6 Mar 2021 13:42:19 +0100
Subject: [PATCH] fix build on Coq 8.11

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

diff --git a/iris/base_logic/lib/ghost_map.v b/iris/base_logic/lib/ghost_map.v
index be21d1865..5e8793c3c 100644
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
@@ -131,7 +131,7 @@ Section lemmas.
   Qed.
   Lemma ghost_map_alloc_strong_empty P :
     pred_infinite P →
-    ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ ghost_map_auth γ 1 ∅.
+    ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ ghost_map_auth γ 1 (∅ : gmap K V).
   Proof.
     intros. iMod (ghost_map_alloc_strong P ∅) as (γ) "(% & Hauth & _)"; eauto.
   Qed.
@@ -143,7 +143,7 @@ Section lemmas.
     - eauto.
   Qed.
   Lemma ghost_map_alloc_empty :
-    ⊢ |==> ∃ γ, ghost_map_auth γ 1 ∅.
+    ⊢ |==> ∃ γ, ghost_map_auth γ 1 (∅ : gmap K V).
   Proof.
     intros. iMod (ghost_map_alloc ∅) as (γ) "(Hauth & _)"; eauto.
   Qed.
-- 
GitLab