From 2056ec6feaa6feba9f8452652e569b12f95e275c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 14 Jul 2022 13:10:46 +0000
Subject: [PATCH] Apply 2 suggestion(s) to 1 file(s)
---
iris/bi/lib/fixpoint.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/iris/bi/lib/fixpoint.v b/iris/bi/lib/fixpoint.v
index f0bc54705..300a46074 100644
--- a/iris/bi/lib/fixpoint.v
+++ b/iris/bi/lib/fixpoint.v
@@ -104,7 +104,7 @@ Section least.
revert x. iApply least_fixpoint_iter; first solve_proper.
iIntros "!> %y #HF !>". iApply least_fixpoint_unfold.
iApply (bi_mono_pred with "[] HF"); first solve_proper.
- by iIntros "!# %x #?".
+ by iIntros "!> %x #?".
Qed.
Lemma least_fixpoint_persistent_absorbing :
@@ -116,7 +116,7 @@ Section least.
iApply least_fixpoint_iter; first solve_proper.
iIntros "!> %y #HF !>". rewrite least_fixpoint_unfold.
iApply (bi_mono_pred with "[] HF"); first solve_proper.
- by iIntros "!# %x #?".
+ by iIntros "!> %x #?".
Qed.
End least.
--
GitLab