diff --git a/theories/base_logic/lib/ghost_var.v b/theories/base_logic/lib/ghost_var.v
index d8e270e00df4288be523cf32993644f726f5fb83..a6af12aff7184c3381ccfa32b660721a60e80371 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.