From 25de501815822ae2e8ae4ff67d6400fbaa402fe2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 23 Dec 2020 15:30:34 +0100
Subject: [PATCH] Remove old FIXMEs.

---
 iris/bi/lib/atomic.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index 2658652ec..471a88906 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -339,8 +339,7 @@ Section lemmas.
       iModIntro. destruct (γ' x'); iApply "HPas"; done.
     - iIntros (y) "Hβ". iMod "Hclose''" as "_".
       iMod ("Hclose'" with "Hβ") as "Hβ'".
-      (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
-      rewrite ->!tele_app_bind. iDestruct "Hβ'" as "[Hβ' HΦ]".
+      rewrite !tele_app_bind. iDestruct "Hβ'" as "[Hβ' HΦ]".
       iMod ("Hclose" with "Hβ'") as "Hγ'".
       iModIntro. destruct (γ' x'); iApply "HΦ"; done.
   Qed.
@@ -375,8 +374,7 @@ Section lemmas.
       iMod ("Hclose" with "Hα"). iApply "Hupd". auto.
     - iIntros (y') "Hβ'". iDestruct "Hclose'" as "[_ Hclose']".
       iMod ("Hclose'" with "Hβ'") as "Hres".
-      (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
-      rewrite ->!tele_app_bind. iDestruct "Hres" as "[[Hα HΦ']|Hcont]".
+      rewrite !tele_app_bind. iDestruct "Hres" as "[[Hα HΦ']|Hcont]".
       + (* Abort the step we are eliminating *)
         iDestruct "Hclose" as "[Hclose _]".
         iMod ("Hclose" with "Hα") as "HP".
-- 
GitLab