From 18ef7b44a095e73eef068f680523a56c6d1dedad Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 28 Dec 2016 12:55:36 +0100
Subject: [PATCH] Issue #55 of iris-coq has been fixed.
---
opam.pins | 2 +-
theories/typing/cont.v | 1 -
2 files changed, 1 insertion(+), 2 deletions(-)
diff --git a/opam.pins b/opam.pins
index dbf958d0..132b6b01 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq fb1712dd9da4d05ca2c919748633801934369d0d
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 5241c33d3013b81bb620b3cfd3cba1f2efdc5b2b
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 22c26a3a..3fc7d459 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -34,7 +34,6 @@ Section typing.
iIntros (args) "Htl HL HT". iApply wp_rec; try done.
{ rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
{ by rewrite -(subst_v_eq (_ :: _) (RecV _ _ _ ::: _)). }
- (* FIXME: iNext here unfolds things in the context. *)
iNext. iApply (Hecont with "* HEAP LFT Htl HE HL [HC] HT").
by iApply "IH".
Qed.
--
GitLab