From b01ac5a8924e012872506014538f369ba6bb4dfc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 24 Jun 2018 11:06:10 +0200
Subject: [PATCH] the rewrite problem now has an issue number

---
 theories/bi/lib/atomic.v        | 4 ++++
 theories/program_logic/atomic.v | 3 ++-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
index 407262be1..59df84626 100644
--- a/theories/bi/lib/atomic.v
+++ b/theories/bi/lib/atomic.v
@@ -326,6 +326,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Φ]".
       iMod ("Hclose" with "Hβ'") as "Hγ'".
       iModIntro. destruct (γ' x'); iApply "HΦ"; done.
@@ -361,6 +362,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]".
       + (* Abort the step we are eliminating *)
         iDestruct "Hclose" as "[Hclose _]".
@@ -399,6 +401,7 @@ Section lemmas.
     iIntros (?) "Hupd Hstep". iApply (aacc_aupd with "Hupd"); first done.
     iIntros (x) "Hα". iApply atomic_acc_wand; last first.
     { iApply "Hstep". done. }
+    (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
     iSplit; first by eauto. iIntros (??) "?". rewrite ->!tele_app_bind. by iRight.
   Qed.
 
@@ -414,6 +417,7 @@ Section lemmas.
     iIntros (?) "Hupd Hstep". iApply (aacc_aupd with "Hupd"); first done.
     iIntros (x) "Hα". iApply atomic_acc_wand; last first.
     { iApply "Hstep". done. }
+    (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
     iSplit; first by eauto. iIntros (??) "?". rewrite ->!tele_app_bind. by iLeft.
   Qed.
 
diff --git a/theories/program_logic/atomic.v b/theories/program_logic/atomic.v
index 8370e5ba5..9c0df1098 100644
--- a/theories/program_logic/atomic.v
+++ b/theories/program_logic/atomic.v
@@ -105,7 +105,7 @@ Section lemmas.
     rewrite ->tforall_forall in HL.
     iIntros "Hwp" (Φ x) "Hα HΦ". iApply ("Hwp" with "[HΦ]"); first iAccu.
     iAuIntro. iAaccIntro with "Hα"; first by eauto. iIntros (y) "Hβ !>".
-    (* FIXME: Using ssreflect rewrite does not work? *)
+    (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
     rewrite ->!tele_app_bind. iIntros "HΦ". iApply "HΦ". done.
   Qed.
 
@@ -120,6 +120,7 @@ Section lemmas.
     iMod ("HΦ") as "[#Hα [Hclose _]]". iMod ("Hclose" with "Hα") as "HΦ".
     iApply wp_fupd. iApply ("Hwp" with "Hα"). iIntros "!>" (y) "Hβ".
     iMod ("HΦ") as "[_ [_ Hclose]]". iMod ("Hclose" with "Hβ") as "HΦ".
+    (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
     rewrite ->!tele_app_bind. iApply "HΦ". done.
   Qed.
 
-- 
GitLab