diff --git a/opam b/opam
index 9d275d4d4009f3a801744388f6606adb3ca12526..e035ade343b792c13e04979f8a60592d5cf4f5ea 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 d99c9d0a4398db011b905338e0b0946ea73dbe49..7c1122d0a064c2bb055fecc878fa6bbb3716b8c3 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]".