From d76fbc01114f293b1201d9b275c9fa31ee7d13c2 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Tue, 15 Sep 2020 17:21:16 -0500
Subject: [PATCH] Fix compilation with Coq 8.10

Fixes a bug from iris/iris!488
---
 theories/base_logic/lib/ghost_var.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/base_logic/lib/ghost_var.v b/theories/base_logic/lib/ghost_var.v
index d8e270e00..a6af12aff 100644
--- a/theories/base_logic/lib/ghost_var.v
+++ b/theories/base_logic/lib/ghost_var.v
@@ -40,7 +40,8 @@ Section lemmas.
     ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ ghost_var γ 1 a.
   Proof.
     iIntros (?). rewrite /ghost_var.
-    iMod (own_alloc_strong _ P) as (γ ?) "Hown"; by eauto.
+    iMod (own_alloc_strong (to_frac_agree (A:=leibnizO A) 1 a) P)
+      as (γ ?) "Hown"; by eauto.
   Qed.
   Lemma ghost_var_alloc a :
     ⊢ |==> ∃ γ, ghost_var γ 1 a.
-- 
GitLab