diff --git a/opam b/opam
index 50566837caee5af7e78ab1f63bb1bb951249cdc5..eb3bb013053bfc70f486f93651f27b76c24ff857 100644
--- a/opam
+++ b/opam
@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2020-02-25.0.55283d57") | (= "dev") }
+  "coq-iris" { (= "dev.2020-02-25.3.bb9152ec") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 17705ae9209906f7b4ae49627a107e417d7af535..1f30e5f0b941fc80f3ed6ea6aaa55423f098fb8b 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -252,7 +252,7 @@ Section code.
       [solve_typing..|].
     iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hclose4]".
     wp_bind (!_)%E. iApply (wp_step_fupd with "[Hshr Hα2β]");
-         [done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
+         [|by iApply ("Hshr" with "[] Hα2β")|]; first done.
     wp_read. iIntros "[#Hshr Hα2β] !>". wp_let.
     iDestruct ("Hclose4" with "Hα2β") as "[Hβ Hα2]".
     iMod ("Hclose3" with "Hβ HL") as "HL".
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 654a10db859d19ffea98a960e5910ff5618222c8..03e65d8a7d3f5d90c28adaedab298c459daad36c 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -695,7 +695,7 @@ Section code.
     - subst strong. wp_op. wp_if. wp_op.
       rewrite shift_loc_0. wp_write. wp_bind (#☠;;#☠)%E.
       iApply (wp_step_fupd with "[Hproto Hrc]");
-        [| |by iApply ("Hproto" with "Hrc")|];
+        [|by iApply ("Hproto" with "Hrc")|];
         [done..|wp_seq; iIntros "(Hty&H†&Hna&Hproto) !>"].
       rewrite <-freeable_sz_full_S, <-(freeable_sz_split _ 2 ty.(ty_size)).
       iDestruct "H†" as "[H†1 H†2]". wp_seq. wp_bind (_<-_;;_)%E.
@@ -790,7 +790,7 @@ Section code.
     iDestruct "Hc" as "[[% [_ Hproto]]|[% [_ Hproto]]]".
     - subst strong. wp_bind (#1 = #1)%E.
       iApply (wp_step_fupd with "[Hproto Hrc]");
-        [| |by iApply ("Hproto" with "Hrc")|];
+        [|by iApply ("Hproto" with "Hrc")|];
         [done..|wp_op; iIntros "(Hty&H†&Hna&Hproto) !>"; wp_if].
       rewrite <-freeable_sz_full_S, <-(freeable_sz_split _ 2 ty.(ty_size)).
       iDestruct "H†" as "[H†1 H†2]". wp_bind (_<-_;;_)%E.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index ae82ed434946c89d54f94ce48a7049969d49f3b7..c9b45260d90a5f081270a59fa0227ac0c63e670e 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -36,7 +36,7 @@ Section refmut_functions.
       [solve_typing..|].
     iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
     wp_bind (!#lx')%E. iApply (wp_step_fupd with "[Hα2β]");
-         [done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
+         [|by iApply ("Hshr" with "[] Hα2β")|]; first done.
     iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β] !>". wp_let.
     iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
     iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1".
@@ -152,7 +152,7 @@ Section refmut_functions.
         iDestruct "Hq" as (q' ?) "?". iExists (q+q')%Qp. iFrame.
         rewrite assoc (comm _ q'' q) //. }
     wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN)); first done.
-    iApply (wp_step_fupd with "INV"); [done|set_solver|]. wp_seq. iIntros "{Hb} Hb !>".
+    iApply (wp_step_fupd with "INV"); [set_solver|]. wp_seq. iIntros "{Hb} Hb !>".
     iMod ("Hcloseβ" with "Hb Hna") as "[Hβ Hna]".
     iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL". wp_seq.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)]
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 2cb00ca6197b2df501d722a7a86031c4f07769b1..b1a160c9f1e4593ede81c7273fb2a175a02e7ee0 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -119,7 +119,7 @@ Section rwlockreadguard_functions.
           { rewrite pos_op_plus -Pplus_one_succ_l Pos.succ_pred // =>?. by subst. }
           rewrite {1}EQn -{1}(agree_idemp (to_agree _)) 2!pair_op Cinr_op Some_op.
           apply (cancel_local_update_unit (reading_st q ν)) , _. }
-      iApply (wp_step_fupd with "INV"). done. set_solver.
+      iApply (wp_step_fupd with "INV"). set_solver.
       iApply (wp_cas_int_suc with "Hlx"); try done. iNext. iIntros "Hlx INV !>".
       iMod ("INV" with "Hlx") as "INV". iMod ("Hcloseβ" with "[$INV]") as "Hβ".
       iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 0646d740d19572cf0df3009721090a32730e649d..45c9edd7362de561d0da7abaef4e5b882319aae5 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -37,7 +37,7 @@ Section rwlockwriteguard_functions.
       [solve_typing..|].
     iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
     wp_bind (!(LitV lx'))%E. iApply (wp_step_fupd with "[Hα2β]");
-         [done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
+         [|by iApply ("Hshr" with "[] Hα2β")|]; first done.
     iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β]!>". wp_op. wp_let.
     iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
     iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1". iMod ("Hclose'" with "Hβ HL") as "HL".
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index a5bea9a88a105d7bf03ec1cabecaa020427791e5..56e7e82544ab6e0acb6cf82a7285c3e6c649d92f 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -168,7 +168,7 @@ Section typing_rules.
     iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
     iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
     iApply (wp_mask_mono _ (↑lftN)); first done.
-    iApply (wp_step_fupd with "Hend"). done. set_solver. wp_seq.
+    iApply (wp_step_fupd with "Hend"); first set_solver. wp_seq.
     iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT HE Htl HL HC [> -]").
     iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
   Qed.