diff --git a/opam b/opam
index 8621367bbad2a705cd282bcda552e08c96189c23..afcf4e22e9dc65ba0881b8d5136fc565c35531e0 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-11-04.0.dca88103") | (= "dev") }
+  "coq-iris" { (= "dev.2020-11-11.0.1346311d") | (= "dev") }
 ]
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index ce0b913eb6fbd22fab2d3bfaa9204be3be0072e0..466eaedb6892b3d4d2844179148bd923770a5296 100644
--- a/theories/examples/map_reduce.v
+++ b/theories/examples/map_reduce.v
@@ -302,7 +302,7 @@ Section mapper.
     wp_apply (par_map_reduce_reduce_spec _ _ [] (Some (i, y, w)) []
       with "[$Hl $Hcsort $Hcred $HIB]"); simpl; auto; [lia|set_solver|].
     iIntros (zs). rewrite /= gmultiset_elements_empty !right_id.
-    iDestruct 1 as (Hzs) "Hk". wp_pures.
+    iDestruct 1 as (Hzs) "Hk".
     iApply ("HΦ" with "[$Hk]"). by rewrite Hzs Hiys.
   Qed.
 End mapper.
diff --git a/theories/examples/par_map.v b/theories/examples/par_map.v
index 807535afd2d1ccdc9ed892d0c02078aaab04da54..638efb9ba66e4b0ae7dc3b1e37b7dafdab27783a 100644
--- a/theories/examples/par_map.v
+++ b/theories/examples/par_map.v
@@ -208,6 +208,6 @@ Section map.
     wp_apply (par_map_client_loop_spec with "[$Hl $Hk $Hc //]"); first lia.
     iIntros (ys) "(?&Hl&Hk)". rewrite /= gmultiset_elements_empty !right_id_L.
     wp_apply (lapp_spec IB _ _ [] with "[$Hl $Hk]"); iIntros "[Hk _] /=".
-    wp_pures. iApply "HΦ"; auto.
+    iApply "HΦ"; auto.
   Qed.
 End map.
diff --git a/theories/examples/sort.v b/theories/examples/sort.v
index 52246e1ab817df7c6e843bff863e753027491f10..7e6da32f8bce5fec9532f087099424b42d3ce428 100644
--- a/theories/examples/sort.v
+++ b/theories/examples/sort.v
@@ -147,6 +147,6 @@ Section sort.
     wp_send with "[$Hcmp]".
     wp_send with "[$Hl]".
     wp_recv (ys) as "(Hsorted & Hperm & Hl)".
-    wp_pures. iApply "HΦ"; iFrame.
+    iApply "HΦ"; iFrame.
   Qed.
 End sort.
diff --git a/theories/examples/sort_fg.v b/theories/examples/sort_fg.v
index 5cd24e11acf889bc134b82919e07e1c20a2aa3e7..af8d0df672fa2e528f5bdd002fb14be9fcb608e5 100644
--- a/theories/examples/sort_fg.v
+++ b/theories/examples/sort_fg.v
@@ -269,7 +269,7 @@ Section sort_fg.
     - wp_recv (y v) as (Htl) "HIx".
       wp_apply ("IH" with "[] Hl Hc"); first by auto using Sorted_snoc.
       iIntros (ys). rewrite -!assoc_L. iDestruct 1 as (??) "[Hl Hc]".
-      wp_apply (lcons_spec with "[$Hl $HIx]"); iIntros "Hl"; wp_pures.
+      wp_apply (lcons_spec with "[$Hl $HIx]"); iIntros "Hl".
       iApply ("HΦ" with "[$Hl $Hc]"); simpl; eauto.
     - iApply ("HΦ" $! []); rewrite /= right_id_L; by iFrame.
   Qed.
diff --git a/theories/logrel/examples/par_recv.v b/theories/logrel/examples/par_recv.v
index 6d55ddfe07b5b782022d79cfb867103fda74d3bf..daba98ef3f9e98912c7e3ea7b8b2b441025462f8 100755
--- a/theories/logrel/examples/par_recv.v
+++ b/theories/logrel/examples/par_recv.v
@@ -96,7 +96,7 @@ Section double.
         eauto.
       + iDestruct "Hc" as "[Hcredit1 Hc]".
         by iDestruct (own_valid_2 with "Hcredit1 Hcredit2") as %[].
-    - iIntros (?? [[x1 ->] [x2 ->]]) "!>". wp_pures. by iApply "HΦ".
+    - iIntros (?? [[x1 ->] [x2 ->]]) "!>". by iApply "HΦ".
   Qed.
 
   Lemma prog_typed :
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 8e69e9ca2021bf90a8fe645ab1f3896725adf44a..f67b1c4d6a3fde96e308a835b7bcdf06b5d6e4ac 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -222,7 +222,7 @@ Section term_typing_rules.
   Proof.
     iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1 /=".
     wp_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[_ HΓ2]". wp_pures.
-    wp_apply (wp_wand with "(He2 HΓ2)"); iIntros (w) "[HB HΓ3]". wp_pures.
+    wp_apply (wp_wand with "(He2 HΓ2)"); iIntros (w) "[HB HΓ3]".
     iFrame "HB HΓ3".
   Qed.