Commit 25de5018 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove old FIXMEs.

parent 9b53243c
......@@ -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".
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment