From c08bba36c9f22e460c03b0edcee975ec12c57495 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 4 Nov 2020 10:25:19 +0100
Subject: [PATCH] =?UTF-8?q?update=20dependencies;=20fix=20for=20`l=20?=
 =?UTF-8?q?=E2=86=A6=20-`=20removal?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 opam                   | 2 +-
 theories/utils/llist.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/opam b/opam
index 9d275d4..e035ade 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
 depends: [
-  "coq-iris" { (= "dev.2020-10-20.2.c65b38ea") | (= "dev") }
+  "coq-iris" { (= "dev.2020-11-03.3.4cd21e62") | (= "dev") }
 ]
diff --git a/theories/utils/llist.v b/theories/utils/llist.v
index d99c9d0..7c1122d 100644
--- a/theories/utils/llist.v
+++ b/theories/utils/llist.v
@@ -193,7 +193,7 @@ Qed.
 Lemma lapp_spec l1 l2 xs1 xs2 :
   {{{ llist I l1 xs1 ∗ llist I l2 xs2 }}}
     lapp #l1 #l2
-  {{{ RET #(); llist I l1 (xs1 ++ xs2) ∗ l2 ↦ - }}}.
+  {{{ RET #(); llist I l1 (xs1 ++ xs2) ∗ (∃ v, l2 ↦ v) }}}.
 Proof.
   iIntros (Φ) "[Hll1 Hll2] HΦ".
   iInduction xs1 as [|x1 xs1] "IH" forall (l1 Φ); simpl; wp_rec; wp_pures.
@@ -209,7 +209,7 @@ Qed.
 Lemma lprep_spec l1 l2 xs1 xs2 :
   {{{ llist I l1 xs2 ∗ llist I l2 xs1 }}}
     lprep #l1 #l2
-  {{{ RET #(); llist I l1 (xs1 ++ xs2) ∗ l2 ↦ - }}}.
+  {{{ RET #(); llist I l1 (xs1 ++ xs2) ∗ (∃ v, l2 ↦ v) }}}.
 Proof.
   iIntros (Φ) "[Hll1 Hll2] HΦ". wp_lam.
   wp_apply (lapp_spec with "[$Hll2 $Hll1]"); iIntros "[Hll2 Hl1]".
-- 
GitLab