From 69f91efcd076e49b8ebee59f362c6c89c6aff9d1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 9 May 2017 19:48:39 +0200
Subject: [PATCH] Remove obsolete FIXME.
---
theories/typing/own.v | 2 --
1 file changed, 2 deletions(-)
diff --git a/theories/typing/own.v b/theories/typing/own.v
index db4fce97..bec0f4a1 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -204,8 +204,6 @@ Section util.
∃ (l : loc) (vl' : vec val m), ⌜v = #l⌝ ∗ ▷ l ↦∗ vl' ∗ ▷ freeable_sz n m l.
Proof.
rewrite ownptr_own. apply uPred.exist_proper=>l. iSplit.
- (* FIXME: The goals here look rather confusing: One cannot tell that we are looking at
- a statement in Iris; the top-level → could just as well be a Coq implication. *)
- iIntros "H". iDestruct "H" as (vl) "(% & Hl & _ & $)". subst v.
iExists vl. iSplit; done.
- iIntros "H". iDestruct "H" as (vl) "(% & Hl & $)". subst v.
--
GitLab