From d7eae97aa4fad623c63c3c8d4cf4f607c7d689ad Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 23 Mar 2022 14:47:37 -0400
Subject: [PATCH] proph_map: fix a variable name

---
 iris/base_logic/lib/proph_map.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/iris/base_logic/lib/proph_map.v b/iris/base_logic/lib/proph_map.v
index f405fa14f..e4e14cf2a 100644
--- a/iris/base_logic/lib/proph_map.v
+++ b/iris/base_logic/lib/proph_map.v
@@ -74,11 +74,11 @@ Section list_resolves.
   Qed.
 End list_resolves.
 
-Lemma proph_map_init `{Countable P, !proph_mapGpreS P V PVS} pvs ps :
-  ⊢ |==> ∃ _ : proph_mapGS P V PVS, proph_map_interp pvs ps.
+Lemma proph_map_init `{Countable P, !proph_mapGpreS P V Σ} pvs ps :
+  ⊢ |==> ∃ _ : proph_mapGS P V Σ, proph_map_interp pvs ps.
 Proof.
   iMod (ghost_map_alloc_empty) as (γ) "Hh".
-  iModIntro. iExists (ProphMapGS P V PVS _ _ _ γ), ∅. iSplit; last by iFrame.
+  iModIntro. iExists (ProphMapGS P V _ _ _ _ γ), ∅. iSplit; last by iFrame.
   iPureIntro. done.
 Qed.
 
-- 
GitLab