From d4dd87167eb93749b4b1516d54e2ab6a05938414 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 8 Nov 2021 15:07:12 -0500
Subject: [PATCH] give some help for using fixpoint_unfold

---
 iris/algebra/ofe.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index c6c31791f..f6119fe6a 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -340,6 +340,9 @@ Definition fixpoint_eq : @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
 Section fixpoint.
   Context `{Cofe A, Inhabited A} (f : A → A) `{!Contractive f}.
 
+  (** This lemma does not work well with [rewrite]; we usually define a specific
+  unfolding lemma for each fixpoint and then [apply fixpoint_unfold] in the
+  proof of that unfolding lemma. *)
   Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f).
   Proof.
     apply equiv_dist=>n.
-- 
GitLab