From 1023ccf75e353b3dd7a4c02ad5be931d5c47f12d Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@groupoid.moe>
Date: Tue, 13 Jun 2023 12:23:28 +0200
Subject: [PATCH] Fix a proof for an older version
---
iris/algebra/local_updates.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/iris/algebra/local_updates.v b/iris/algebra/local_updates.v
index 6eb0a090c..87a436473 100644
--- a/iris/algebra/local_updates.v
+++ b/iris/algebra/local_updates.v
@@ -154,7 +154,7 @@ Proof.
eapply Hupd, Hg; eauto.
- specialize (Hupd i).
rewrite local_update_unital in Hupd.
- eapply Hupd; eauto.
+ eapply Hupd, Hg; eauto.
Qed.
(** * Product *)
--
GitLab