diff --git a/opam b/opam
index 8b3aee447fd1a531481e93996096b542565465ba..2d74ba79a9363d62f723354f00fe6bb427a4519b 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dev.2018-05-23.0.4fc7ee79") | (= "dev") }
+  "coq-iris" { (= "dev.2018-05-23.1.b043f3a3") | (= "dev") }
 ]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index d2bde800832fd4183a9927611efb5972f2779dba..fd04e13dd101e930522a8153cbe9cbf341b5ef17 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -141,7 +141,7 @@ Section heap.
 
   Lemma heap_mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
   Proof.
-    rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid uPred.discrete_valid.
+    rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
     eapply pure_elim; [done|]=> /auth_own_valid /=.
     rewrite op_singleton pair_op singleton_valid=> -[? /agree_op_invL'->]; eauto.
   Qed.
@@ -461,7 +461,7 @@ Section heap.
     ==∗ own heap_name (● to_heap (<[l:=(RSt (n2 + nf), v)]> σ))
         ∗ heap_mapsto_st (RSt n2) l q v.
   Proof.
-    intros Hσv. apply uPred.wand_intro_r. rewrite -!own_op to_heap_insert.
+    intros Hσv. apply wand_intro_r. rewrite -!own_op to_heap_insert.
     eapply own_update, auth_update, singleton_local_update.
     { by rewrite /to_heap lookup_fmap Hσv. }
     apply prod_local_update_1, prod_local_update_2, csum_local_update_r.
@@ -510,7 +510,7 @@ Section heap.
     ==∗ own heap_name (● to_heap (<[l:=(st2, v')]> σ))
         ∗ heap_mapsto_st st2 l 1%Qp v'.
   Proof.
-    intros Hσv. apply uPred.wand_intro_r. rewrite -!own_op to_heap_insert.
+    intros Hσv. apply wand_intro_r. rewrite -!own_op to_heap_insert.
     eapply own_update, auth_update, singleton_local_update.
     { by rewrite /to_heap lookup_fmap Hσv. }
     apply exclusive_local_update. by destruct st2.
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 31301b9da52746d3e62357cf2090e69827e2e865..f37ad06df23304491332a9d9d9bfa8ecab5fd554 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -120,7 +120,7 @@ Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
 Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
   match e with
   | Val v e H => Val v e H
-  | @ClosedExpr e H => @ClosedExpr e H
+  | ClosedExpr e => ClosedExpr e
   | Var y => if bool_decide (y = x) then es else Var y
   | Lit l => Lit l
   | Rec f xl e =>