From 770bb016c8fa644676539c66ce55d189336a76c0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 24 Sep 2021 14:30:21 -0400
Subject: [PATCH] get rid of unnecessary OfeMor

---
 iris/base_logic/lib/saved_prop.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/base_logic/lib/saved_prop.v b/iris/base_logic/lib/saved_prop.v
index 51c2892da..85df42832 100644
--- a/iris/base_logic/lib/saved_prop.v
+++ b/iris/base_logic/lib/saved_prop.v
@@ -98,7 +98,7 @@ Notation savedPredG Σ A := (savedAnythingG Σ (A -d> ▶ ∙)).
 Notation savedPredΣ A := (savedAnythingΣ (A -d> ▶ ∙)).
 
 Definition saved_pred_own `{!savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ) :=
-  saved_anything_own (F := A -d> ▶ ∙) γ (OfeMor Next ∘ Φ).
+  saved_anything_own (F := A -d> ▶ ∙) γ (Next ∘ Φ).
 
 Global Instance saved_pred_own_contractive `{!savedPredG Σ A} γ :
   Contractive (saved_pred_own γ : (A -d> iPropO Σ) → iProp Σ).
-- 
GitLab